![]() |
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 9587 | . 2 ⊢ ω ∈ V | |
2 | omelon2 7819 | . 2 ⊢ (ω ∈ V → ω ∈ On) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ω ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3447 Oncon0 6321 ωcom 7806 |
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 2704 ax-sep 5260 ax-nul 5267 ax-pr 5388 ax-un 7676 ax-inf2 9585 |
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 2711 df-cleq 2725 df-clel 2811 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3933 df-nul 4287 df-if 4491 df-pw 4566 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-br 5110 df-opab 5172 df-tr 5227 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5592 df-we 5594 df-ord 6324 df-on 6325 df-lim 6326 df-suc 6327 df-om 7807 |
This theorem is referenced by: oancom 9595 cnfcomlem 9643 cnfcom 9644 cnfcom2lem 9645 cnfcom2 9646 cnfcom3lem 9647 cnfcom3 9648 cnfcom3clem 9649 cardom 9930 infxpenlem 9957 xpomen 9959 infxpidm2 9961 infxpenc 9962 infxpenc2lem1 9963 infxpenc2 9966 alephon 10013 infenaleph 10035 iunfictbso 10058 dfac12k 10091 infunsdom1 10157 domtriomlem 10386 iunctb 10518 pwcfsdom 10527 canthp1lem2 10597 pwfseqlem4a 10605 pwfseqlem4 10606 pwfseqlem5 10607 wunex3 10685 znnen 16102 qnnen 16103 cygctb 19677 2ndcctbss 22829 2ndcomap 22832 2ndcsep 22833 tx1stc 23024 tx2ndc 23025 met1stc 23900 met2ndci 23901 re2ndc 24187 uniiccdif 24965 dyadmbl 24987 opnmblALT 24990 mbfimaopnlem 25042 aannenlem3 25713 exrecfnlem 35900 poimirlem32 36160 numinfctb 41477 onexomgt 41622 onexlimgt 41624 onexoegt 41625 1oaomeqom 41675 oaabsb 41676 oaordnrex 41677 oaordnr 41678 2omomeqom 41685 omnord1ex 41686 omnord1 41687 nnoeomeqom 41694 oenord1 41698 oaomoencom 41699 cantnftermord 41702 cantnfub 41703 cantnf2 41707 nnawordexg 41709 dflim5 41711 oacl2g 41712 onmcl 41713 omabs2 41714 omcl2 41715 ofoaf 41718 ofoafo 41719 naddcnff 41725 naddcnffo 41727 naddcnfcom 41729 naddcnfid1 41730 naddcnfid2 41731 naddcnfass 41732 naddwordnexlem0 41760 naddwordnexlem1 41761 naddwordnexlem3 41763 oawordex3 41764 naddwordnexlem4 41765 infordmin 41896 minregex 41898 omiscard 41907 sucomisnotcard 41908 aleph1min 41921 alephiso3 41923 |
Copyright terms: Public domain | W3C validator |