Theorem onelon 6357

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Ord word 6331  Oncon0 6332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336

This theorem is referenced by:  oneli  6448  ssorduni  7755  unon  7806  tfindsg2  7838  dfom2  7844  trom  7851  onfununi  8310  onnseq  8313  dfrecs3  8341  tz7.48-2  8410  tz7.49  8413  oalim  8496  omlim  8497  oelim  8498  oaordi  8510  oalimcl  8524  oaass  8525  omordi  8530  omlimcl  8542  odi  8543  omass  8544  omeulem1  8546  omeulem2  8547  omopth2  8548  oewordri  8556  oeordsuc  8558  oelimcl  8564  oeeui  8566  oaabs2  8613  omabs  8615  naddssim  8649  naddel12  8664  naddsuc2  8665  omxpenlem  9042  hartogs  9497  card2on  9507  cantnfle  9624  cantnflt  9625  cantnfp1lem3  9633  cantnfp1  9634  oemapvali  9637  cantnflem1b  9639  cantnflem1c  9640  cantnflem1d  9641  cantnflem1  9642  cantnflem2  9643  cantnflem3  9644  cantnflem4  9645  cantnf  9646  cnfcomlem  9652  cnfcom3lem  9656  cnfcom3  9657  r1ordg  9731  r1val3  9791  tskwe  9903  iscard  9928  cardmin2  9952  infxpenlem  9966  infxpenc2lem2  9973  alephordi  10027  alephord2i  10030  alephle  10041  cardaleph  10042  cfub  10202  cfsmolem  10223  zorn2lem5  10453  zorn2lem6  10454  ttukeylem6  10467  ttukeylem7  10468  ondomon  10516  cardmin  10517  alephval2  10525  alephreg  10535  smobeth  10539  winainflem  10646  inar1  10728  inatsk  10731  sltval2  27568  sltres  27574  nosepeq  27597  nosupno  27615  nosupres  27619  nosupbnd1lem1  27620  nosupbnd2lem1  27627  nosupbnd2  27628  noinfno  27630  noinfres  27634  noinfbnd1lem1  27635  noinfbnd2lem1  27642  noinfbnd2  27643  oldlim  27798  oldbday  27812  dfrdg2  35783  dfrdg4  35939  ontopbas  36416  onpsstopbas  36418  onint1  36437  onelord  43240  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