Theorem omelon 9684

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.)

Assertion

Ref	Expression
omelon	⊢ ω ∈ On

Proof of Theorem omelon

Step	Hyp	Ref	Expression
1		omex 9681	. 2 ⊢ ω ∈ V
2		omelon2 7900	. 2 ⊢ (ω ∈ V → ω ∈ On)
3	1, 2	ax-mp 5	1 ⊢ ω ∈ On

Syntax hints:   ∈ wcel 2106  Vcvv 3478  Oncon0 6386  ωcom 7887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754  ax-inf2 9679

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-om 7888

This theorem is referenced by:  oancom  9689  cnfcomlem  9737  cnfcom  9738  cnfcom2lem  9739  cnfcom2  9740  cnfcom3lem  9741  cnfcom3  9742  cnfcom3clem  9743  cardom  10024  infxpenlem  10051  xpomen  10053  infxpidm2  10055  infxpenc  10056  infxpenc2lem1  10057  infxpenc2  10060  alephon  10107  infenaleph  10129  iunfictbso  10152  dfac12k  10186  infunsdom1  10250  domtriomlem  10480  iunctb  10612  pwcfsdom  10621  canthp1lem2  10691  pwfseqlem4a  10699  pwfseqlem4  10700  pwfseqlem5  10701  wunex3  10779  znnen  16245  qnnen  16246  cygctb  19925  2ndcctbss  23479  2ndcomap  23482  2ndcsep  23483  tx1stc  23674  tx2ndc  23675  met1stc  24550  met2ndci  24551  re2ndc  24837  uniiccdif  25627  dyadmbl  25649  opnmblALT  25652  mbfimaopnlem  25704  aannenlem3  26387  n0ssold  28370  exrecfnlem  37362  poimirlem32  37639  numinfctb  43092  onexomgt  43230  onexlimgt  43232  onexoegt  43233  1oaomeqom  43283  oaabsb  43284  oaordnrex  43285  oaordnr  43286  2omomeqom  43293  omnord1ex  43294  omnord1  43295  nnoeomeqom  43302  oenord1  43306  oaomoencom  43307  cantnftermord  43310  cantnfub  43311  cantnf2  43315  nnawordexg  43317  dflim5  43319  oacl2g  43320  onmcl  43321  omabs2  43322  omcl2  43323  tfsnfin  43342  ofoaf  43345  ofoafo  43346  naddcnff  43352  naddcnffo  43354  naddcnfcom  43356  naddcnfid1  43357  naddcnfid2  43358  naddcnfass  43359  naddwordnexlem0  43386  naddwordnexlem1  43387  naddwordnexlem3  43389  oawordex3  43390  naddwordnexlem4  43391  infordmin  43522  minregex  43524  omiscard  43533  sucomisnotcard  43534  aleph1min  43547  alephiso3  43549