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 | ⊢ 1𝑜 ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 7447 | . 2 ⊢ 1𝑜 = suc ∅ | |
2 | 0elon 5695 | . . 3 ⊢ ∅ ∈ On | |
3 | 2 | onsuci 6930 | . 2 ⊢ suc ∅ ∈ On |
4 | 1, 3 | eqeltri 2684 | 1 ⊢ 1𝑜 ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 ∅c0 3874 Oncon0 5640 suc csuc 5642 1𝑜c1o 7440 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-tr 4681 df-eprel 4949 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-ord 5643 df-on 5644 df-suc 5646 df-1o 7447 |
This theorem is referenced by: 2on 7455 ondif2 7469 2oconcl 7470 fnoe 7477 oev 7481 oe0 7489 oev2 7490 oesuclem 7492 oecl 7504 o1p1e2 7507 o2p2e4 7508 om1r 7510 oe1m 7512 omword1 7540 omword2 7541 omlimcl 7545 oneo 7548 oewordi 7558 oelim2 7562 oeoa 7564 oeoe 7566 oeeui 7569 oaabs2 7612 endisj 7932 sdom1 8045 sucxpdom 8054 oancom 8431 cnfcom3lem 8483 pm54.43lem 8708 pm54.43 8709 infxpenc 8724 infxpenc2 8728 uncdadom 8876 cdaun 8877 cdaen 8878 cda1dif 8881 pm110.643 8882 pm110.643ALT 8883 cdacomen 8886 cdaassen 8887 xpcdaen 8888 mapcdaen 8889 cdaxpdom 8894 cdafi 8895 cdainf 8897 infcda1 8898 pwcda1 8899 pwcdadom 8921 cfsuc 8962 isfin4-3 9020 dcomex 9152 pwcfsdom 9284 pwxpndom2 9366 wunex2 9439 wuncval2 9448 tsk2 9466 sadcf 15013 sadcp1 15015 xpscg 16041 xpscfn 16042 xpsc0 16043 xpsc1 16044 xpsfrnel 16046 xpsfrnel2 16048 xpsle 16064 efgmnvl 17950 efgi1 17957 frgpuptinv 18007 frgpnabllem1 18099 dmdprdpr 18271 dprdpr 18272 psr1crng 19378 psr1assa 19379 psr1tos 19380 psr1bas 19382 vr1cl2 19384 ply1lss 19387 ply1subrg 19388 coe1fval3 19399 ressply1bas2 19419 ressply1add 19421 ressply1mul 19422 ressply1vsca 19423 subrgply1 19424 00ply1bas 19431 ply1plusgfvi 19433 psr1ring 19438 psr1lmod 19440 psr1sca 19441 ply1ascl 19449 subrg1ascl 19450 subrg1asclcl 19451 subrgvr1 19452 subrgvr1cl 19453 coe1z 19454 coe1mul2lem1 19458 coe1mul2 19460 coe1tm 19464 evls1val 19506 evls1rhm 19508 evls1sca 19509 evl1val 19514 evl1rhm 19517 evl1sca 19519 evl1var 19521 evls1var 19523 mpfpf1 19536 pf1mpf 19537 pf1ind 19540 xkofvcn 21297 xpstopnlem1 21422 xpstopnlem2 21424 ufildom1 21540 xpsdsval 21996 deg1z 23651 deg1addle 23665 deg1vscale 23668 deg1vsca 23669 deg1mulle2 23673 deg1le0 23675 ply1nzb 23686 sltval2 31053 nofv 31054 noxp1o 31063 sltsolem1 31067 bdayfo 31074 nobnddown 31100 rankeq1o 31448 ssoninhaus 31617 onint1 31618 finxp1o 32405 finxpreclem3 32406 finxpreclem4 32407 finxpreclem5 32408 finxpsuclem 32410 pw2f1ocnv 36622 wepwsolem 36630 pwfi2f1o 36684 clsk3nimkb 37358 clsk1indlem4 37362 clsk1indlem1 37363 ply1ass23l 41964 |
Copyright terms: Public domain | W3C validator |