![]() |
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.) Avoid ax-un 7708. (Revised by BTernaryTau, 30-Nov-2024.) |
Ref | Expression |
---|---|
2on | ⊢ 2o ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2o 8449 | . 2 ⊢ 2o = suc 1o | |
2 | 1on 8460 | . . 3 ⊢ 1o ∈ On | |
3 | 2oex 8459 | . . . 4 ⊢ 2o ∈ V | |
4 | 1, 3 | eqeltrri 2829 | . . 3 ⊢ suc 1o ∈ V |
5 | sucexeloni 7780 | . . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On) | |
6 | 2, 4, 5 | mp2an 690 | . 2 ⊢ suc 1o ∈ On |
7 | 1, 6 | eqeltri 2828 | 1 ⊢ 2o ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3473 Oncon0 6353 suc csuc 6355 1oc1o 8441 2oc2o 8442 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-br 5142 df-opab 5204 df-tr 5259 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-ord 6356 df-on 6357 df-suc 6359 df-1o 8448 df-2o 8449 |
This theorem is referenced by: ord3 8465 3on 8466 ord2eln012 8479 o2p2e4 8523 o2p2e4OLD 8524 oneo 8564 2onn 8624 nneob 8638 en3 9265 infxpenc 9995 infxpenc2 9999 mappwen 10089 pwdjuen 10158 ackbij1lem5 10201 sdom2en01 10279 fin1a2lem4 10380 fin1a2lem6 10382 xpsrnbas 17499 xpsadd 17502 xpsmul 17503 xpsvsca 17505 xpsle 17507 cat1 18029 xpsmnd 18642 xpsgrp 18916 efgval 19549 efgtf 19554 frgpcpbl 19591 frgp0 19592 frgpeccl 19593 frgpadd 19595 frgpmhm 19597 vrgpf 19600 vrgpinv 19601 frgpupf 19605 frgpup1 19607 frgpup2 19608 frgpup3lem 19609 frgpnabllem1 19701 frgpnabllem2 19702 xpstopnlem1 23242 xpstps 23243 xpstopnlem2 23244 xpsxmetlem 23814 xpsdsval 23816 nofv 27087 sltres 27092 noextendgt 27100 nolesgn2ores 27102 nosepnelem 27109 nosepdmlem 27113 nolt02o 27125 nogt01o 27126 nosupno 27133 nosupbnd1lem3 27140 nosupbnd1 27144 nosupbnd2lem1 27145 nosupbnd2 27146 ssoninhaus 35137 onint1 35138 1oequni2o 36053 finxpreclem4 36079 pw2f1ocnv 41547 frlmpwfi 41611 omnord1 41826 oege2 41828 oenord1 41837 oaomoencom 41838 oenassex 41839 oenass 41840 omabs2 41853 oaltom 41927 omltoe 41929 2no 41959 nlim3 41966 tr3dom 42050 enrelmap 42519 |
Copyright terms: Public domain | W3C validator |