Theorem omelon 9625

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  Oncon0 6351  ωcom 7860

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734  ax-inf2 9620

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-om 7861

This theorem is used by:  oancom  9630  cnfcomlem  9678  cnfcom  9679  cnfcom2lem  9680  cnfcom2  9681  cnfcom3lem  9682  cnfcom3  9683  cnfcom3clem  9684  cardom  10038  infxpenlem  10063  xpomen  10065  infxpidm2  10067  infxpenc  10068  infxpenc2lem1  10069  infxpenc2  10072  alephon  10119  infenaleph  10141  iunfictbso  10164  dfac12k  10197  infunsdom1  10261  domtriomlem  10491  dmct  10573  fimact  10586  fnct  10591  iunctb  10630  pwcfsdom  10639  canthp1lem2  10709  pwfseqlem4a  10717  pwfseqlem4  10718  pwfseqlem5  10719  wunex3  10797  znnen  16347  qnnen  16348  cygctb  20067  2ndcctbss  23735  2ndcomap  23738  2ndcsep  23739  tx1stc  23930  tx2ndc  23931  met1stc  24801  met2ndci  24802  re2ndc  25081  uniiccdif  25860  dyadmbl  25882  opnmblALT  25885  mbfimaopnlem  25937  aannenlem3  26620  dfz12s2  28807  exrecfnlem  38222  poimirlem32  38490  numinfctb  44048  onexomgt  44186  onexlimgt  44188  onexoegt  44189  1oaomeqom  44238  oaabsb  44239  oaordnrex  44240  oaordnr  44241  2omomeqom  44248  omnord1ex  44249  omnord1  44250  nnoeomeqom  44257  oenord1  44261  oaomoencom  44262  cantnftermord  44265  cantnfub  44266  cantnf2  44270  nnawordexg  44272  dflim5  44274  oacl2g  44275  onmcl  44276  omabs2  44277  omcl2  44278  tfsnfin  44297  ofoaf  44300  ofoafo  44301  naddcnff  44307  naddcnffo  44309  naddcnfcom  44311  naddcnfid1  44312  naddcnfid2  44313  naddcnfass  44314  naddwordnexlem0  44341  naddwordnexlem1  44342  naddwordnexlem3  44344  oawordex3  44345  naddwordnexlem4  44346  infordmin  44476  minregex  44478  omiscard  44487  sucomisnotcard  44488  aleph1min  44501  alephiso3  44503  wfaxinf2  45928  subsaliuncl  47290  smflimlem6  47708