![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2on | Structured version Visualization version GIF version |
Description: Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
Ref | Expression |
---|---|
2on | ⊢ 2o ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2o 8086 | . 2 ⊢ 2o = suc 1o | |
2 | 1on 8092 | . . 3 ⊢ 1o ∈ On | |
3 | 2 | onsuci 7533 | . 2 ⊢ suc 1o ∈ On |
4 | 1, 3 | eqeltri 2886 | 1 ⊢ 2o ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 Oncon0 6159 suc csuc 6161 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-suc 6165 df-1o 8085 df-2o 8086 |
This theorem is referenced by: 3on 8097 o2p2e4 8149 o2p2e4OLD 8150 oneo 8190 nneob 8262 infxpenc 9429 infxpenc2 9433 mappwen 9523 pwdjuen 9592 ackbij1lem5 9635 sdom2en01 9713 fin1a2lem4 9814 fin1a2lem6 9816 xpsrnbas 16836 xpsadd 16839 xpsmul 16840 xpsvsca 16842 xpsle 16844 xpsmnd 17943 xpsgrp 18210 efgval 18835 efgtf 18840 frgpcpbl 18877 frgp0 18878 frgpeccl 18879 frgpadd 18881 frgpmhm 18883 vrgpf 18886 vrgpinv 18887 frgpupf 18891 frgpup1 18893 frgpup2 18894 frgpup3lem 18895 frgpnabllem1 18986 frgpnabllem2 18987 xpstopnlem1 22414 xpstps 22415 xpstopnlem2 22416 xpsxmetlem 22986 xpsdsval 22988 nofv 33277 sltres 33282 noextendgt 33290 nolesgn2ores 33292 nosepnelem 33297 nosepdmlem 33300 nolt02o 33312 nosupno 33316 nosupbday 33318 nosupbnd1lem3 33323 nosupbnd1 33327 nosupbnd2lem1 33328 nosupbnd2 33329 ssoninhaus 33909 onint1 33910 1oequni2o 34785 finxpreclem4 34811 pw2f1ocnv 39978 frlmpwfi 40042 tr3dom 40236 enrelmap 40698 |
Copyright terms: Public domain | W3C validator |