Theorem omelon 9599

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  Oncon0 6332  ωcom 7842

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-inf2 9594

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-om 7843

This theorem is referenced by:  oancom  9604  cnfcomlem  9652  cnfcom  9653  cnfcom2lem  9654  cnfcom2  9655  cnfcom3lem  9656  cnfcom3  9657  cnfcom3clem  9658  cardom  9939  infxpenlem  9966  xpomen  9968  infxpidm2  9970  infxpenc  9971  infxpenc2lem1  9972  infxpenc2  9975  alephon  10022  infenaleph  10044  iunfictbso  10067  dfac12k  10101  infunsdom1  10165  domtriomlem  10395  iunctb  10527  pwcfsdom  10536  canthp1lem2  10606  pwfseqlem4a  10614  pwfseqlem4  10615  pwfseqlem5  10616  wunex3  10694  znnen  16180  qnnen  16181  cygctb  19822  2ndcctbss  23342  2ndcomap  23345  2ndcsep  23346  tx1stc  23537  tx2ndc  23538  met1stc  24409  met2ndci  24410  re2ndc  24689  uniiccdif  25479  dyadmbl  25501  opnmblALT  25504  mbfimaopnlem  25556  aannenlem3  26238  n0ssold  28245  exrecfnlem  37367  poimirlem32  37646  numinfctb  43092  onexomgt  43230  onexlimgt  43232  onexoegt  43233  1oaomeqom  43282  oaabsb  43283  oaordnrex  43284  oaordnr  43285  2omomeqom  43292  omnord1ex  43293  omnord1  43294  nnoeomeqom  43301  oenord1  43305  oaomoencom  43306  cantnftermord  43309  cantnfub  43310  cantnf2  43314  nnawordexg  43316  dflim5  43318  oacl2g  43319  onmcl  43320  omabs2  43321  omcl2  43322  tfsnfin  43341  ofoaf  43344  ofoafo  43345  naddcnff  43351  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfid2  43357  naddcnfass  43358  naddwordnexlem0  43385  naddwordnexlem1  43386  naddwordnexlem3  43388  oawordex3  43389  naddwordnexlem4  43390  infordmin  43521  minregex  43523  omiscard  43532  sucomisnotcard  43533  aleph1min  43546  alephiso3  43548  wfaxinf2  44991