![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2onn | Structured version Visualization version GIF version |
Description: The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.) |
Ref | Expression |
---|---|
2onn | ⊢ 2o ∈ ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2o 8086 | . 2 ⊢ 2o = suc 1o | |
2 | 1onn 8248 | . . 3 ⊢ 1o ∈ ω | |
3 | peano2 7582 | . . 3 ⊢ (1o ∈ ω → suc 1o ∈ ω) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ suc 1o ∈ ω |
5 | 1, 4 | eqeltri 2886 | 1 ⊢ 2o ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 suc csuc 6161 ωcom 7560 1oc1o 8078 2oc2o 8079 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-tr 5137 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-om 7561 df-1o 8085 df-2o 8086 |
This theorem is referenced by: 3onn 8250 nn2m 8260 nnneo 8261 nneob 8262 omopthlem1 8265 omopthlem2 8266 pwen 8674 en3 8739 en2eqpr 9418 en2eleq 9419 unctb 9616 infdjuabs 9617 ackbij1lem5 9635 sdom2en01 9713 fin56 9804 fin67 9806 fin1a2lem4 9814 alephexp1 9990 pwcfsdom 9994 alephom 9996 canthp1lem2 10064 pwxpndom2 10076 hash3 13763 hash2pr 13823 pr2pwpr 13833 rpnnen 15572 rexpen 15573 xpsfrnel 16827 xpscf 16830 symggen 18590 psgnunilem1 18613 simpgnsgd 19215 znfld 20252 hauspwdom 22106 xpsmet 22989 xpsxms 23141 xpsms 23142 unidifsnel 30307 unidifsnne 30308 sat1el2xp 32739 ex-sategoelelomsuc 32786 ex-sategoelel12 32787 1oequni2o 34785 finxpreclem4 34811 finxp3o 34817 wepwso 39987 frlmpwfi 40042 |
Copyright terms: Public domain | W3C validator |