Theorem onelon 6410

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

Assertion

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

Proof of Theorem onelon

Step	Hyp	Ref	Expression
1		eloni 6395	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelon 6409	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
3	1, 2	sylan 580	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  Ord word 6384  Oncon0 6385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389

This theorem is referenced by:  oneli  6499  ssorduni  7797  unon  7850  tfindsg2  7882  dfom2  7888  trom  7895  onfununi  8379  onnseq  8382  dfrecs3  8410  dfrecs3OLD  8411  tz7.48-2  8480  tz7.49  8483  oalim  8568  omlim  8569  oelim  8570  oaordi  8582  oalimcl  8596  oaass  8597  omordi  8602  omlimcl  8614  odi  8615  omass  8616  omeulem1  8618  omeulem2  8619  omopth2  8620  oewordri  8628  oeordsuc  8630  oelimcl  8636  oeeui  8638  oaabs2  8685  omabs  8687  naddssim  8721  naddel12  8736  naddsuc2  8737  omxpenlem  9111  hartogs  9581  card2on  9591  cantnfle  9708  cantnflt  9709  cantnfp1lem3  9717  cantnfp1  9718  oemapvali  9721  cantnflem1b  9723  cantnflem1c  9724  cantnflem1d  9725  cantnflem1  9726  cantnflem2  9727  cantnflem3  9728  cantnflem4  9729  cantnf  9730  cnfcomlem  9736  cnfcom3lem  9740  cnfcom3  9741  r1ordg  9815  r1val3  9875  tskwe  9987  iscard  10012  cardmin2  10036  infxpenlem  10050  infxpenc2lem2  10057  alephordi  10111  alephord2i  10114  alephle  10125  cardaleph  10126  cfub  10286  cfsmolem  10307  zorn2lem5  10537  zorn2lem6  10538  ttukeylem6  10551  ttukeylem7  10552  ondomon  10600  cardmin  10601  alephval2  10609  alephreg  10619  smobeth  10623  winainflem  10730  inar1  10812  inatsk  10815  sltval2  27715  sltres  27721  nosepeq  27744  nosupno  27762  nosupres  27766  nosupbnd1lem1  27767  nosupbnd2lem1  27774  nosupbnd2  27775  noinfno  27777  noinfres  27781  noinfbnd1lem1  27782  noinfbnd2lem1  27789  noinfbnd2  27790  oldlim  27939  oldbday  27953  dfrdg2  35776  dfrdg4  35932  ontopbas  36410  onpsstopbas  36412  onint1  36431  onelord  43239  cantnfresb  43313  oawordex2  43315  oacl2g  43319  omabs2  43321  omcl2  43322  tfsconcatfv2  43329  tfsconcatfv  43330  tfsconcatrn  43331  tfsconcat0i  43334  ofoafg  43343  ofoaass  43349  oaun3lem1  43363  oaun3lem2  43364  oadif1lem  43368  oadif1  43369  nadd2rabtr  43373  nadd1suc  43381  naddgeoa  43383  naddwordnexlem0  43385  naddwordnexlem1  43386  naddwordnexlem3  43388  oawordex3  43389  naddwordnexlem4  43390  omssrncard  43529