![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > omelon | Structured version Visualization version GIF version |
Description: Omega is an ordinal number. Theorem 1.22 of [Schloeder] p. 3. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.) |
Ref | Expression |
---|---|
omelon | ⊢ ω ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omex 9668 | . 2 ⊢ ω ∈ V | |
2 | omelon2 7884 | . 2 ⊢ (ω ∈ V → ω ∈ On) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ω ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 Vcvv 3461 Oncon0 6371 ωcom 7871 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 ax-un 7741 ax-inf2 9666 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-tr 5267 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-om 7872 |
This theorem is referenced by: oancom 9676 cnfcomlem 9724 cnfcom 9725 cnfcom2lem 9726 cnfcom2 9727 cnfcom3lem 9728 cnfcom3 9729 cnfcom3clem 9730 cardom 10011 infxpenlem 10038 xpomen 10040 infxpidm2 10042 infxpenc 10043 infxpenc2lem1 10044 infxpenc2 10047 alephon 10094 infenaleph 10116 iunfictbso 10139 dfac12k 10172 infunsdom1 10238 domtriomlem 10467 iunctb 10599 pwcfsdom 10608 canthp1lem2 10678 pwfseqlem4a 10686 pwfseqlem4 10687 pwfseqlem5 10688 wunex3 10766 znnen 16192 qnnen 16193 cygctb 19859 2ndcctbss 23403 2ndcomap 23406 2ndcsep 23407 tx1stc 23598 tx2ndc 23599 met1stc 24474 met2ndci 24475 re2ndc 24761 uniiccdif 25551 dyadmbl 25573 opnmblALT 25576 mbfimaopnlem 25628 aannenlem3 26310 n0ssold 28270 exrecfnlem 36989 poimirlem32 37256 numinfctb 42669 onexomgt 42811 onexlimgt 42813 onexoegt 42814 1oaomeqom 42864 oaabsb 42865 oaordnrex 42866 oaordnr 42867 2omomeqom 42874 omnord1ex 42875 omnord1 42876 nnoeomeqom 42883 oenord1 42887 oaomoencom 42888 cantnftermord 42891 cantnfub 42892 cantnf2 42896 nnawordexg 42898 dflim5 42900 oacl2g 42901 onmcl 42902 omabs2 42903 omcl2 42904 tfsnfin 42923 ofoaf 42926 ofoafo 42927 naddcnff 42933 naddcnffo 42935 naddcnfcom 42937 naddcnfid1 42938 naddcnfid2 42939 naddcnfass 42940 naddwordnexlem0 42968 naddwordnexlem1 42969 naddwordnexlem3 42971 oawordex3 42972 naddwordnexlem4 42973 infordmin 43104 minregex 43106 omiscard 43115 sucomisnotcard 43116 aleph1min 43129 alephiso3 43131 |
Copyright terms: Public domain | W3C validator |