Theorem onelon 6313

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 6298	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelon 6312	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
3	1, 2	sylan 580	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105  Ord word 6287  Oncon0 6288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rab 3404  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-tr 5204  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-we 5564  df-ord 6291  df-on 6292

This theorem is referenced by:  oneli  6400  ssorduni  7670  unon  7722  tfindsg2  7754  dfom2  7760  trom  7767  onfununi  8220  onnseq  8223  dfrecs3  8251  dfrecs3OLD  8252  tz7.48-2  8321  tz7.49  8324  oalim  8411  omlim  8412  oelim  8413  oaordi  8426  oalimcl  8440  oaass  8441  omordi  8446  omlimcl  8458  odi  8459  omass  8460  omeulem1  8462  omeulem2  8463  omopth2  8464  oewordri  8472  oeordsuc  8474  oelimcl  8480  oeeui  8482  oaabs2  8528  omabs  8530  omxpenlem  8916  hartogs  9379  card2on  9389  cantnfle  9506  cantnflt  9507  cantnfp1lem3  9515  cantnfp1  9516  oemapvali  9519  cantnflem1b  9521  cantnflem1c  9522  cantnflem1d  9523  cantnflem1  9524  cantnflem2  9525  cantnflem3  9526  cantnflem4  9527  cantnf  9528  cnfcomlem  9534  cnfcom3lem  9538  cnfcom3  9539  r1ordg  9613  r1val3  9673  tskwe  9785  iscard  9810  cardmin2  9834  infxpenlem  9848  infxpenc2lem2  9855  alephordi  9909  alephord2i  9912  alephle  9923  cardaleph  9924  cfub  10084  cfsmolem  10105  zorn2lem5  10335  zorn2lem6  10336  ttukeylem6  10349  ttukeylem7  10350  ondomon  10398  cardmin  10399  alephval2  10407  alephreg  10417  smobeth  10421  winainflem  10528  inar1  10610  inatsk  10613  sltval2  26884  sltres  26890  nosepeq  26913  dfrdg2  33898  naddssim  33960  nosupno  33976  nosupres  33980  nosupbnd1lem1  33981  nosupbnd2lem1  33988  nosupbnd2  33989  noinfno  33991  noinfres  33995  noinfbnd1lem1  33996  noinfbnd2lem1  34003  noinfbnd2  34004  oldlim  34139  oldbday  34151  dfrdg4  34323  ontopbas  34687  onpsstopbas  34689  onint1  34708  oacl2g  41270  ofoafg  41271  ofoaass  41277  omssrncard  41386