nnsdom - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem nnsdom 4635

Description: A natural number is strictly dominated by the set of natural numbers.

**Assertion**
Ref	Expression
nnsdom

**Proof of Theorem nnsdom**
Step	Hyp	Ref	Expression
1		omsdomnn 4530	. . 3 $/\$
2		omex 4627	. . . . . 6
3	2	ensym 4412	. . . . 5
4	3	con3i 98	. . . 4
5	4	anim2i 335	. . 3 $/\$ $/\$
6	1, 5	syl 10	. 2 $/\$
7		brsdom 4381	. 2 $/\$
8	6, 7	sylibr 200	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3 $/\$ wa 223

wcel 958 class class class wbr 2619

com 3131

cen 4364

cdom 4365

csdm 4366

This theorem is referenced by: cardom 4825 sucdom 4842 alephexp1 7584

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-9 965 ax-10 966 ax-11 967 ax-12 968 ax-13 969 ax-14 970 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-rep 2693 ax-sep 2703 ax-nul 2710 ax-pow 2742 ax-pr 2779 ax-un 2866 ax-inf2 4625

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 776 df-3an 777 df-ex 981 df-sb 1172 df-eu 1382 df-mo 1383 df-clab 1464 df-cleq 1469 df-clel 1472 df-ne 1587 df-ral 1649 df-rex 1650 df-v 1812 df-dif 2049 df-un 2050 df-in 2051 df-ss 2053 df-pss 2055 df-nul 2281 df-if 2362 df-pw 2402 df-sn 2412 df-pr 2413 df-tp 2415 df-op 2416 df-uni 2504 df-br 2620 df-opab 2667 df-tr 2681 df-eprel 2832 df-id 2835 df-po 2840 df-so 2850 df-fr 2917 df-we 2934 df-ord 2951 df-on 2952 df-lim 2953 df-suc 2954 df-om 3132 df-xp 3184 df-rel 3185 df-cnv 3186 df-co 3187 df-dm 3188 df-rn 3189 df-res 3190 df-ima 3191 df-fun 3192 df-fn 3193 df-f 3194 df-f1 3195 df-fo 3196 df-f1o 3197 df-fv 3198 df-er 4261 df-en 4368 df-dom 4369 df-sdom 4370