Theorem omelon 9542

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 9539	. 2 ⊢ ω ∈ V
2		omelon2 7815	. 2 ⊢ (ω ∈ V → ω ∈ On)
3	1, 2	ax-mp 5	1 ⊢ ω ∈ On

Syntax hints:   ∈ wcel 2111  Vcvv 3436  Oncon0 6312  ωcom 7802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-inf2 9537

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-tr 5201  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-om 7803

This theorem is referenced by:  oancom  9547  cnfcomlem  9595  cnfcom  9596  cnfcom2lem  9597  cnfcom2  9598  cnfcom3lem  9599  cnfcom3  9600  cnfcom3clem  9601  cardom  9885  infxpenlem  9910  xpomen  9912  infxpidm2  9914  infxpenc  9915  infxpenc2lem1  9916  infxpenc2  9919  alephon  9966  infenaleph  9988  iunfictbso  10011  dfac12k  10045  infunsdom1  10109  domtriomlem  10339  iunctb  10471  pwcfsdom  10480  canthp1lem2  10550  pwfseqlem4a  10558  pwfseqlem4  10559  pwfseqlem5  10560  wunex3  10638  znnen  16127  qnnen  16128  cygctb  19810  2ndcctbss  23376  2ndcomap  23379  2ndcsep  23380  tx1stc  23571  tx2ndc  23572  met1stc  24442  met2ndci  24443  re2ndc  24722  uniiccdif  25512  dyadmbl  25534  opnmblALT  25537  mbfimaopnlem  25589  aannenlem3  26271  n0ssold  28287  exrecfnlem  37430  poimirlem32  37698  numinfctb  43201  onexomgt  43339  onexlimgt  43341  onexoegt  43342  1oaomeqom  43391  oaabsb  43392  oaordnrex  43393  oaordnr  43394  2omomeqom  43401  omnord1ex  43402  omnord1  43403  nnoeomeqom  43410  oenord1  43414  oaomoencom  43415  cantnftermord  43418  cantnfub  43419  cantnf2  43423  nnawordexg  43425  dflim5  43427  oacl2g  43428  onmcl  43429  omabs2  43430  omcl2  43431  tfsnfin  43450  ofoaf  43453  ofoafo  43454  naddcnff  43460  naddcnffo  43462  naddcnfcom  43464  naddcnfid1  43465  naddcnfid2  43466  naddcnfass  43467  naddwordnexlem0  43494  naddwordnexlem1  43495  naddwordnexlem3  43497  oawordex3  43498  naddwordnexlem4  43499  infordmin  43630  minregex  43632  omiscard  43641  sucomisnotcard  43642  aleph1min  43655  alephiso3  43657  wfaxinf2  45099