Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem cardom 3632

Description: The set of natural numbers is a cardinal number. Theorem 18.11 of [Monk1] p. 133.

**Assertion**
Ref	Expression
cardom

**Proof of Theorem cardom**
Step	Hyp	Ref	Expression
1		omelon 3476	. . . 4
2		oncardid 3628	. . . 4
3	1, 2	ax-mp 6	. . 3
4		nnsdom 3481	. . . 4
5		sdomnen 3291	. . . 4
6	4, 5	syl 12	. . 3
7	3, 6	mt2 96	. 2
8		cardonle 3629	. . . . 5
9	1, 8	ax-mp 6	. . . 4
10		oncardon 3627	. . . . . 6
11	1, 10	ax-mp 6	. . . . 5
12	11, 1	onssel 2357	. . . 4 $\/$
13	9, 12	mpbi 164	. . 3 $\/$
14	13	ori 200	. 2
15	7, 14	ax-mp 6	1

Colors of variables: wff set class

Syntax hints:

wn 1 $\/$ wo 195

wceq 1091

wcel 1092

wss 1487 class class class wbr 2054

con0 2199

com 2372

cfv 2422

cen 3271

csdm 3273

ccrd 3620

This theorem is referenced by: alephcard 3673 cfom 3710

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-er 3200 df-en 3274 df-dom 3275 df-sdom 3276 df-card 3623