![]() |
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 7673. (Revised by BTernaryTau, 30-Nov-2024.) |
Ref | Expression |
---|---|
2on | ⊢ 2o ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2o 8414 | . 2 ⊢ 2o = suc 1o | |
2 | 1on 8425 | . . 3 ⊢ 1o ∈ On | |
3 | 2oex 8424 | . . . 4 ⊢ 2o ∈ V | |
4 | 1, 3 | eqeltrri 2835 | . . 3 ⊢ suc 1o ∈ V |
5 | sucexeloni 7745 | . . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On) | |
6 | 2, 4, 5 | mp2an 691 | . 2 ⊢ suc 1o ∈ On |
7 | 1, 6 | eqeltri 2834 | 1 ⊢ 2o ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3446 Oncon0 6318 suc csuc 6320 1oc1o 8406 2oc2o 8407 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-ral 3066 df-rex 3075 df-rab 3409 df-v 3448 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3930 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-tr 5224 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5589 df-we 5591 df-ord 6321 df-on 6322 df-suc 6324 df-1o 8413 df-2o 8414 |
This theorem is referenced by: ord3 8430 3on 8431 ord2eln012 8444 o2p2e4 8488 o2p2e4OLD 8489 oneo 8529 2onn 8589 nneob 8603 en3 9227 infxpenc 9955 infxpenc2 9959 mappwen 10049 pwdjuen 10118 ackbij1lem5 10161 sdom2en01 10239 fin1a2lem4 10340 fin1a2lem6 10342 xpsrnbas 17454 xpsadd 17457 xpsmul 17458 xpsvsca 17460 xpsle 17462 cat1 17984 xpsmnd 18597 xpsgrp 18867 efgval 19500 efgtf 19505 frgpcpbl 19542 frgp0 19543 frgpeccl 19544 frgpadd 19546 frgpmhm 19548 vrgpf 19551 vrgpinv 19552 frgpupf 19556 frgpup1 19558 frgpup2 19559 frgpup3lem 19560 frgpnabllem1 19652 frgpnabllem2 19653 xpstopnlem1 23163 xpstps 23164 xpstopnlem2 23165 xpsxmetlem 23735 xpsdsval 23737 nofv 27008 sltres 27013 noextendgt 27021 nolesgn2ores 27023 nosepnelem 27030 nosepdmlem 27034 nolt02o 27046 nogt01o 27047 nosupno 27054 nosupbnd1lem3 27061 nosupbnd1 27065 nosupbnd2lem1 27066 nosupbnd2 27067 ssoninhaus 34923 onint1 34924 1oequni2o 35842 finxpreclem4 35868 pw2f1ocnv 41364 frlmpwfi 41428 omnord1 41642 oege2 41644 oenord1 41653 oaomoencom 41654 oenassex 41655 oenass 41656 omabs2 41668 2no 41716 nlim3 41723 tr3dom 41807 enrelmap 42276 |
Copyright terms: Public domain | W3C validator |