![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2onn | Unicode version |
Description: The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.) |
Ref | Expression |
---|---|
2onn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2o 6432 |
. 2
![]() ![]() ![]() ![]() ![]() | |
2 | 1onn 6535 |
. . 3
![]() ![]() ![]() ![]() | |
3 | peano2 4606 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | ax-mp 5 |
. 2
![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2260 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 |
This theorem depends on definitions: df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-rex 2471 df-v 2751 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-pw 3589 df-sn 3610 df-pr 3611 df-uni 3822 df-int 3857 df-suc 4383 df-iom 4602 df-1o 6431 df-2o 6432 |
This theorem is referenced by: 3onn 6537 2ssom 6539 nn2m 6542 pw1fin 6924 nninfex 7134 infnninfOLD 7137 nnnninf 7138 isomnimap 7149 enomnilem 7150 fodjuf 7157 ismkvmap 7166 ismkvnex 7167 enmkvlem 7173 iswomnimap 7178 enwomnilem 7181 nninfdcinf 7183 nninfwlporlem 7185 nninfwlpoimlemg 7187 exmidonfinlem 7206 exmidfodomrlemr 7215 exmidfodomrlemrALT 7216 pw1ne3 7243 3nsssucpw1 7249 2onetap 7268 2omotaplemap 7270 2omotaplemst 7271 exmidmotap 7274 prarloclemarch2 7432 nq02m 7478 prarloclemlt 7506 prarloclemlo 7507 prarloclem3 7510 prarloclemn 7512 prarloclem5 7513 prarloclemcalc 7515 hash3 10807 unct 12457 xpsfrnel 12782 xpscf 12785 2o01f 15043 pwle2 15045 pwf1oexmid 15046 subctctexmid 15047 0nninf 15050 nnsf 15051 nninfsellemdc 15056 nninfself 15059 nninffeq 15066 isomninnlem 15075 iswomninnlem 15094 ismkvnnlem 15097 |
Copyright terms: Public domain | W3C validator |