Theorem onelon 6048

Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)

Assertion

Ref	Expression
onelon	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Proof of Theorem onelon

Step	Hyp	Ref	Expression
1		eloni 6033	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelon 6047	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
3	1, 2	sylan 572	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2048  Ord word 6022  Oncon0 6023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pr 5180

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-tr 5025  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-we 5361  df-ord 6026  df-on 6027

This theorem is referenced by:  oneli  6130  ssorduni  7310  unon  7356  tfindsg2  7386  dfom2  7392  ordom  7399  onfununi  7775  onnseq  7778  dfrecs3  7806  tz7.48-2  7874  tz7.49  7877  oalim  7951  omlim  7952  oelim  7953  oaordi  7965  oalimcl  7979  oaass  7980  omordi  7985  omlimcl  7997  odi  7998  omass  7999  omeulem1  8001  omeulem2  8002  omopth2  8003  oewordri  8011  oeordsuc  8013  oelimcl  8019  oeeui  8021  oaabs2  8064  omabs  8066  omxpenlem  8406  hartogs  8795  card2on  8805  cantnfle  8920  cantnflt  8921  cantnfp1lem3  8929  cantnfp1  8930  oemapvali  8933  cantnflem1b  8935  cantnflem1c  8936  cantnflem1d  8937  cantnflem1  8938  cantnflem2  8939  cantnflem3  8940  cantnflem4  8941  cantnf  8942  cnfcomlem  8948  cnfcom3lem  8952  cnfcom3  8953  r1ordg  8993  r1val3  9053  tskwe  9165  iscard  9190  cardmin2  9213  infxpenlem  9225  infxpenc2lem2  9232  alephordi  9286  alephord2i  9289  alephle  9300  cardaleph  9301  cfub  9461  cfsmolem  9482  zorn2lem5  9712  zorn2lem6  9713  ttukeylem6  9726  ttukeylem7  9727  ondomon  9775  cardmin  9776  alephval2  9784  alephreg  9794  smobeth  9798  winainflem  9905  inar1  9987  inatsk  9990  dfrdg2  32501  sltval2  32624  sltres  32630  nosepeq  32650  nosupno  32664  nosupres  32668  nosupbnd1lem1  32669  nosupbnd2lem1  32676  nosupbnd2  32677  dfrdg4  32873  ontopbas  33236  onpsstopbas  33238  onint1  33257