Theorem omelon 9674

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  Oncon0 6380  ωcom 7901

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775  ax-inf2 9669

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-tr 5216  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-om 7902

This theorem is used by:  oancom  9679  cnfcomlem  9727  cnfcom  9728  cnfcom2lem  9729  cnfcom2  9730  cnfcom3lem  9731  cnfcom3  9732  cnfcom3clem  9733  cardom  10094  infxpenlem  10119  xpomen  10121  infxpidm2  10123  infxpenc  10124  infxpenc2lem1  10125  infxpenc2  10128  alephon  10175  infenaleph  10197  iunfictbso  10220  dfac12k  10253  infunsdom1  10317  domtriomlem  10547  dmct  10629  fimact  10642  fnct  10647  iunctb  10686  pwcfsdom  10695  canthp1lem2  10765  pwfseqlem4a  10773  pwfseqlem4  10774  pwfseqlem5  10775  wunex3  10853  znnen  16409  qnnen  16410  cygctb  20136  2ndcctbss  23804  2ndcomap  23807  2ndcsep  23808  tx1stc  23999  tx2ndc  24000  met1stc  24870  met2ndci  24871  re2ndc  25150  uniiccdif  25929  dyadmbl  25951  opnmblALT  25954  mbfimaopnlem  26006  aannenlem3  26687  dfz12s2  28904  j0ltaleph  36008  exrecfnlem  38494  poimirlem32  38762  numinfctb  44297  onexomgt  44435  onexlimgt  44437  onexoegt  44438  1oaomeqom  44487  oaabsb  44488  oaordnrex  44489  oaordnr  44490  2omomeqom  44497  omnord1ex  44498  omnord1  44499  nnoeomeqom  44506  oenord1  44510  oaomoencom  44511  cantnftermord  44514  cantnfub  44515  cantnf2  44519  nnawordexg  44521  dflim5  44523  oacl2g  44524  onmcl  44525  omabs2  44526  omcl2  44527  tfsnfin  44546  ofoaf  44549  ofoafo  44550  naddcnff  44556  naddcnffo  44558  naddcnfcom  44560  naddcnfid1  44561  naddcnfid2  44562  naddcnfass  44563  naddwordnexlem0  44590  naddwordnexlem1  44591  naddwordnexlem3  44593  oawordex3  44594  naddwordnexlem4  44595  infordmin  44725  minregex  44727  omiscard  44736  sucomisnotcard  44737  aleph1min  44750  alephiso3  44752  wfaxinf2  46186  subsaliuncl  47573  smflimlem6  47991