| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 1on | Structured version Visualization version GIF version | ||
| Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7755. (Revised by BTernaryTau, 30-Nov-2024.) |
| Ref | Expression |
|---|---|
| 1on | ⊢ 1o ∈ On |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-1o 8506 | . 2 ⊢ 1o = suc ∅ | |
| 2 | 0elon 6438 | . . 3 ⊢ ∅ ∈ On | |
| 3 | 1oex 8516 | . . . 4 ⊢ 1o ∈ V | |
| 4 | 1, 3 | eqeltrri 2838 | . . 3 ⊢ suc ∅ ∈ V |
| 5 | sucexeloni 7829 | . . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On) | |
| 6 | 2, 4, 5 | mp2an 692 | . 2 ⊢ suc ∅ ∈ On |
| 7 | 1, 6 | eqeltri 2837 | 1 ⊢ 1o ∈ On |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ∅c0 4333 Oncon0 6384 suc csuc 6386 1oc1o 8499 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-tr 5260 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-ord 6387 df-on 6388 df-suc 6390 df-1o 8506 |
| This theorem is referenced by: 2on 8520 2onOLD 8521 nlim2 8528 ord1eln01 8534 ondif2 8540 2oconcl 8541 fnoe 8548 oesuclem 8563 oecl 8575 o1p1e2 8578 om1r 8581 oe1m 8583 omword1 8611 omword2 8612 omlimcl 8616 oneo 8619 oewordi 8629 oelim2 8633 oeoa 8635 oeoe 8637 oeeui 8640 1onn 8678 oaabs2 8687 enpr2dOLD 9090 sucxpdom 9291 en2 9315 oancom 9691 cnfcom3lem 9743 ssttrcl 9755 ttrcltr 9756 dmttrcl 9761 ttrclselem2 9766 pm54.43lem 10040 pm54.43 10041 infxpenc 10058 infxpenc2 10062 undjudom 10208 endjudisj 10209 djuen 10210 dju1p1e2 10214 dju1p1e2ALT 10215 xpdjuen 10220 mapdjuen 10221 djuxpdom 10226 djufi 10227 djuinf 10229 infdju1 10230 pwdju1 10231 pwdjudom 10255 isfin4p1 10355 pwxpndom2 10705 wunex2 10778 wuncval2 10787 tsk2 10805 efgmnvl 19732 frgpnabllem1 19891 dmdprdpr 20069 dprdpr 20070 psr1crng 22188 psr1assa 22189 psr1tos 22190 psr1bas 22192 vr1cl2 22194 ply1lss 22198 ply1subrg 22199 ply1ass23l 22228 ressply1bas2 22229 ressply1add 22231 ressply1mul 22232 ressply1vsca 22233 subrgply1 22234 ply1plusgfvi 22243 psr1ring 22248 psr1lmod 22250 psr1sca 22251 ply1ascl 22261 subrg1ascl 22262 subrg1asclcl 22263 subrgvr1 22264 subrgvr1cl 22265 coe1z 22266 coe1mul2lem1 22270 coe1mul2 22272 coe1tm 22276 evls1val 22324 evls1rhm 22326 evls1sca 22327 evl1val 22333 evl1rhm 22336 evl1sca 22338 evl1var 22340 evls1var 22342 mpfpf1 22355 pf1mpf 22356 pf1ind 22359 xkofvcn 23692 xpstopnlem1 23817 ufildom1 23934 deg1z 26126 deg1addle 26140 deg1vscale 26143 deg1vsca 26144 deg1mulle2 26148 deg1le0 26150 ply1nzb 26162 sltval2 27701 noextendlt 27714 sltsolem1 27720 nosepnelem 27724 nolt02o 27740 old1 27914 rankeq1o 36172 ssoninhaus 36449 onint1 36450 1oequni2o 37369 finxp1o 37393 finxpreclem3 37394 finxpreclem4 37395 finxpreclem5 37396 finxpsuclem 37398 pw2f1ocnv 43049 wepwsolem 43054 pwfi2f1o 43108 oaabsb 43307 oaordnr 43309 omnord1 43318 oege1 43319 oaomoencom 43330 omabs2 43345 omcl3g 43347 nadd1suc 43405 om2 43417 oe2 43419 safesnsupfiss 43428 safesnsupfidom1o 43430 safesnsupfilb 43431 1no 43449 nlim2NEW 43456 oa1cl 43460 sn1dom 43539 pr2dom 43540 tr3dom 43541 clsk1indlem4 44057 |
| Copyright terms: Public domain | W3C validator |