![]() |
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 36260 poimirlem32 36520 numinfctb 41845 onexomgt 41990 onexlimgt 41992 onexoegt 41993 1oaomeqom 42043 oaabsb 42044 oaordnrex 42045 oaordnr 42046 2omomeqom 42053 omnord1ex 42054 omnord1 42055 nnoeomeqom 42062 oenord1 42066 oaomoencom 42067 cantnftermord 42070 cantnfub 42071 cantnf2 42075 nnawordexg 42077 dflim5 42079 oacl2g 42080 onmcl 42081 omabs2 42082 omcl2 42083 tfsnfin 42102 ofoaf 42105 ofoafo 42106 naddcnff 42112 naddcnffo 42114 naddcnfcom 42116 naddcnfid1 42117 naddcnfid2 42118 naddcnfass 42119 naddwordnexlem0 42147 naddwordnexlem1 42148 naddwordnexlem3 42150 oawordex3 42151 naddwordnexlem4 42152 infordmin 42283 minregex 42285 omiscard 42294 sucomisnotcard 42295 aleph1min 42308 alephiso3 42310 |
Copyright terms: Public domain | W3C validator |