Theorem omelon 9686

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  Oncon0 6384  ωcom 7887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-inf2 9681

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-om 7888

This theorem is referenced by:  oancom  9691  cnfcomlem  9739  cnfcom  9740  cnfcom2lem  9741  cnfcom2  9742  cnfcom3lem  9743  cnfcom3  9744  cnfcom3clem  9745  cardom  10026  infxpenlem  10053  xpomen  10055  infxpidm2  10057  infxpenc  10058  infxpenc2lem1  10059  infxpenc2  10062  alephon  10109  infenaleph  10131  iunfictbso  10154  dfac12k  10188  infunsdom1  10252  domtriomlem  10482  iunctb  10614  pwcfsdom  10623  canthp1lem2  10693  pwfseqlem4a  10701  pwfseqlem4  10702  pwfseqlem5  10703  wunex3  10781  znnen  16248  qnnen  16249  cygctb  19910  2ndcctbss  23463  2ndcomap  23466  2ndcsep  23467  tx1stc  23658  tx2ndc  23659  met1stc  24534  met2ndci  24535  re2ndc  24822  uniiccdif  25613  dyadmbl  25635  opnmblALT  25638  mbfimaopnlem  25690  aannenlem3  26372  n0ssold  28355  exrecfnlem  37380  poimirlem32  37659  numinfctb  43115  onexomgt  43253  onexlimgt  43255  onexoegt  43256  1oaomeqom  43306  oaabsb  43307  oaordnrex  43308  oaordnr  43309  2omomeqom  43316  omnord1ex  43317  omnord1  43318  nnoeomeqom  43325  oenord1  43329  oaomoencom  43330  cantnftermord  43333  cantnfub  43334  cantnf2  43338  nnawordexg  43340  dflim5  43342  oacl2g  43343  onmcl  43344  omabs2  43345  omcl2  43346  tfsnfin  43365  ofoaf  43368  ofoafo  43369  naddcnff  43375  naddcnffo  43377  naddcnfcom  43379  naddcnfid1  43380  naddcnfid2  43381  naddcnfass  43382  naddwordnexlem0  43409  naddwordnexlem1  43410  naddwordnexlem3  43412  oawordex3  43413  naddwordnexlem4  43414  infordmin  43545  minregex  43547  omiscard  43556  sucomisnotcard  43557  aleph1min  43570  alephiso3  43572  wfaxinf2  45018