Theorem onelon 6409

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Ord word 6383  Oncon0 6384

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388

This theorem is referenced by:  oneli  6498  ssorduni  7799  unon  7851  tfindsg2  7883  dfom2  7889  trom  7896  onfununi  8381  onnseq  8384  dfrecs3  8412  dfrecs3OLD  8413  tz7.48-2  8482  tz7.49  8485  oalim  8570  omlim  8571  oelim  8572  oaordi  8584  oalimcl  8598  oaass  8599  omordi  8604  omlimcl  8616  odi  8617  omass  8618  omeulem1  8620  omeulem2  8621  omopth2  8622  oewordri  8630  oeordsuc  8632  oelimcl  8638  oeeui  8640  oaabs2  8687  omabs  8689  naddssim  8723  naddel12  8738  naddsuc2  8739  omxpenlem  9113  hartogs  9584  card2on  9594  cantnfle  9711  cantnflt  9712  cantnfp1lem3  9720  cantnfp1  9721  oemapvali  9724  cantnflem1b  9726  cantnflem1c  9727  cantnflem1d  9728  cantnflem1  9729  cantnflem2  9730  cantnflem3  9731  cantnflem4  9732  cantnf  9733  cnfcomlem  9739  cnfcom3lem  9743  cnfcom3  9744  r1ordg  9818  r1val3  9878  tskwe  9990  iscard  10015  cardmin2  10039  infxpenlem  10053  infxpenc2lem2  10060  alephordi  10114  alephord2i  10117  alephle  10128  cardaleph  10129  cfub  10289  cfsmolem  10310  zorn2lem5  10540  zorn2lem6  10541  ttukeylem6  10554  ttukeylem7  10555  ondomon  10603  cardmin  10604  alephval2  10612  alephreg  10622  smobeth  10626  winainflem  10733  inar1  10815  inatsk  10818  sltval2  27701  sltres  27707  nosepeq  27730  nosupno  27748  nosupres  27752  nosupbnd1lem1  27753  nosupbnd2lem1  27760  nosupbnd2  27761  noinfno  27763  noinfres  27767  noinfbnd1lem1  27768  noinfbnd2lem1  27775  noinfbnd2  27776  oldlim  27925  oldbday  27939  dfrdg2  35796  dfrdg4  35952  ontopbas  36429  onpsstopbas  36431  onint1  36450  onelord  43263  cantnfresb  43337  oawordex2  43339  oacl2g  43343  omabs2  43345  omcl2  43346  tfsconcatfv2  43353  tfsconcatfv  43354  tfsconcatrn  43355  tfsconcat0i  43358  ofoafg  43367  ofoaass  43373  oaun3lem1  43387  oaun3lem2  43388  oadif1lem  43392  oadif1  43393  nadd2rabtr  43397  nadd1suc  43405  naddgeoa  43407  naddwordnexlem0  43409  naddwordnexlem1  43410  naddwordnexlem3  43412  oawordex3  43413  naddwordnexlem4  43414  omssrncard  43553