![]() |
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 9638 | . 2 ⊢ ω ∈ V | |
2 | omelon2 7868 | . 2 ⊢ (ω ∈ V → ω ∈ On) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ω ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3475 Oncon0 6365 ωcom 7855 |
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 5300 ax-nul 5307 ax-pr 5428 ax-un 7725 ax-inf2 9636 |
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 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-tr 5267 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-om 7856 |
This theorem is referenced by: oancom 9646 cnfcomlem 9694 cnfcom 9695 cnfcom2lem 9696 cnfcom2 9697 cnfcom3lem 9698 cnfcom3 9699 cnfcom3clem 9700 cardom 9981 infxpenlem 10008 xpomen 10010 infxpidm2 10012 infxpenc 10013 infxpenc2lem1 10014 infxpenc2 10017 alephon 10064 infenaleph 10086 iunfictbso 10109 dfac12k 10142 infunsdom1 10208 domtriomlem 10437 iunctb 10569 pwcfsdom 10578 canthp1lem2 10648 pwfseqlem4a 10656 pwfseqlem4 10657 pwfseqlem5 10658 wunex3 10736 znnen 16155 qnnen 16156 cygctb 19760 2ndcctbss 22959 2ndcomap 22962 2ndcsep 22963 tx1stc 23154 tx2ndc 23155 met1stc 24030 met2ndci 24031 re2ndc 24317 uniiccdif 25095 dyadmbl 25117 opnmblALT 25120 mbfimaopnlem 25172 aannenlem3 25843 exrecfnlem 36308 poimirlem32 36568 numinfctb 41893 onexomgt 42038 onexlimgt 42040 onexoegt 42041 1oaomeqom 42091 oaabsb 42092 oaordnrex 42093 oaordnr 42094 2omomeqom 42101 omnord1ex 42102 omnord1 42103 nnoeomeqom 42110 oenord1 42114 oaomoencom 42115 cantnftermord 42118 cantnfub 42119 cantnf2 42123 nnawordexg 42125 dflim5 42127 oacl2g 42128 onmcl 42129 omabs2 42130 omcl2 42131 tfsnfin 42150 ofoaf 42153 ofoafo 42154 naddcnff 42160 naddcnffo 42162 naddcnfcom 42164 naddcnfid1 42165 naddcnfid2 42166 naddcnfass 42167 naddwordnexlem0 42195 naddwordnexlem1 42196 naddwordnexlem3 42198 oawordex3 42199 naddwordnexlem4 42200 infordmin 42331 minregex 42333 omiscard 42342 sucomisnotcard 42343 aleph1min 42356 alephiso3 42358 |
Copyright terms: Public domain | W3C validator |