HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The set of natural numbers is a cardinal number. Theorem 18.11 of [Monk1] p. 133. |
| Ref | Expression |
|---|---|
| cardom |
       |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | omelon 4775 |
. . . 4
  | |
| 2 | oncardid 4967 |
. . . 4
  | |
| 3 | 1, 2 | ax-mp 7 |
. . 3
|
| 4 | nnsdom 4781 |
. . . 4
 | |
| 5 | sdomnen 4528 |
. . . 4
 | |
| 6 | 4, 5 | syl 10 |
. . 3
|
| 7 | 3, 6 | mt2 108 |
. 2
|
| 8 | cardonle 4968 |
. . . . 5
 | |
| 9 | 1, 8 | ax-mp 7 |
. . . 4
|
| 10 | oncardon 4966 |
. . . . . 6
| |
| 11 | 1, 10 | ax-mp 7 |
. . . . 5
|
| 12 | 11, 1 | onsseli 3084 |
. . . 4
  |
| 13 | 9, 12 | mpbi 187 |
. . 3
|
| 14 | 13 | ori 228 |
. 2
|
| 15 | 7, 14 | ax-mp 7 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 2
wo 220
wceq 992
wcel 994
wss 2099
class class class wbr 2692 con0 2975 com 3218 cfv 3263 cen 4505 csdm 4507 ccrd 4959 |
| This theorem is referenced by: alephcard 5017 alephval2 5052 cfom 5066 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089 ax-inf2 4770 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-ral 1695 df-rex 1696 df-rab 1698 df-v 1858 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-pss 2107 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-int 2601 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-lim 2980 df-suc 2981 df-om 3219 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-er 4401 df-en 4509 df-dom 4510 df-sdom 4511 df-fin 4512 df-card 4962 |