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.) |
Ref | Expression |
---|---|
1on | ⊢ 1o ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 8093 | . 2 ⊢ 1o = suc ∅ | |
2 | 0elon 6238 | . . 3 ⊢ ∅ ∈ On | |
3 | 2 | onsuci 7541 | . 2 ⊢ suc ∅ ∈ On |
4 | 1, 3 | eqeltri 2909 | 1 ⊢ 1o ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ∅c0 4290 Oncon0 6185 suc csuc 6187 1oc1o 8086 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-tp 4564 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-tr 5165 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-ord 6188 df-on 6189 df-suc 6191 df-1o 8093 |
This theorem is referenced by: 1oex 8101 2on 8102 ondif2 8118 2oconcl 8119 fnoe 8126 oesuclem 8141 oecl 8153 o1p1e2 8156 o2p2e4 8157 om1r 8159 oe1m 8161 omword1 8189 omword2 8190 omlimcl 8194 oneo 8197 oewordi 8207 oelim2 8211 oeoa 8213 oeoe 8215 oeeui 8218 oaabs2 8262 enpr2d 8586 sucxpdom 8716 oancom 9103 cnfcom3lem 9155 pm54.43lem 9417 pm54.43 9418 infxpenc 9433 infxpenc2 9437 undjudom 9582 endjudisj 9583 djuen 9584 dju1p1e2 9588 dju1p1e2ALT 9589 xpdjuen 9594 mapdjuen 9595 djuxpdom 9600 djufi 9601 djuinf 9603 infdju1 9604 pwdju1 9605 pwdjudom 9627 isfin4p1 9726 pwxpndom2 10076 wunex2 10149 wuncval2 10158 tsk2 10176 efgmnvl 18771 frgpnabllem1 18924 dmdprdpr 19102 dprdpr 19103 psr1crng 20285 psr1assa 20286 psr1tos 20287 psr1bas 20289 vr1cl2 20291 ply1lss 20294 ply1subrg 20295 ressply1bas2 20326 ressply1add 20328 ressply1mul 20329 ressply1vsca 20330 subrgply1 20331 ply1plusgfvi 20340 psr1ring 20345 psr1lmod 20347 psr1sca 20348 ply1ascl 20356 subrg1ascl 20357 subrg1asclcl 20358 subrgvr1 20359 subrgvr1cl 20360 coe1z 20361 coe1mul2lem1 20365 coe1mul2 20367 coe1tm 20371 evls1val 20413 evls1rhm 20415 evls1sca 20416 evl1val 20422 evl1rhm 20425 evl1sca 20427 evl1var 20429 evls1var 20431 mpfpf1 20444 pf1mpf 20445 pf1ind 20448 xkofvcn 22222 xpstopnlem1 22347 ufildom1 22464 deg1z 24610 deg1addle 24624 deg1vscale 24627 deg1vsca 24628 deg1mulle2 24632 deg1le0 24634 ply1nzb 24645 sltval2 33061 noextendlt 33074 sltsolem1 33078 nosepnelem 33082 nolt02o 33097 rankeq1o 33530 ssoninhaus 33694 onint1 33695 1oequni2o 34532 finxp1o 34556 finxpreclem3 34557 finxpreclem4 34558 finxpreclem5 34559 finxpsuclem 34561 pw2f1ocnv 39514 wepwsolem 39522 pwfi2f1o 39576 sn1dom 39772 pr2dom 39773 tr3dom 39774 clsk1indlem4 40274 ply1ass23l 44334 |
Copyright terms: Public domain | W3C validator |