Theorem onelon 6377

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Ord word 6351  Oncon0 6352

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356

This theorem is referenced by:  oneli  6467  ssorduni  7771  unon  7823  tfindsg2  7855  dfom2  7861  trom  7868  onfununi  8353  onnseq  8356  dfrecs3  8384  dfrecs3OLD  8385  tz7.48-2  8454  tz7.49  8457  oalim  8542  omlim  8543  oelim  8544  oaordi  8556  oalimcl  8570  oaass  8571  omordi  8576  omlimcl  8588  odi  8589  omass  8590  omeulem1  8592  omeulem2  8593  omopth2  8594  oewordri  8602  oeordsuc  8604  oelimcl  8610  oeeui  8612  oaabs2  8659  omabs  8661  naddssim  8695  naddel12  8710  naddsuc2  8711  omxpenlem  9085  hartogs  9556  card2on  9566  cantnfle  9683  cantnflt  9684  cantnfp1lem3  9692  cantnfp1  9693  oemapvali  9696  cantnflem1b  9698  cantnflem1c  9699  cantnflem1d  9700  cantnflem1  9701  cantnflem2  9702  cantnflem3  9703  cantnflem4  9704  cantnf  9705  cnfcomlem  9711  cnfcom3lem  9715  cnfcom3  9716  r1ordg  9790  r1val3  9850  tskwe  9962  iscard  9987  cardmin2  10011  infxpenlem  10025  infxpenc2lem2  10032  alephordi  10086  alephord2i  10089  alephle  10100  cardaleph  10101  cfub  10261  cfsmolem  10282  zorn2lem5  10512  zorn2lem6  10513  ttukeylem6  10526  ttukeylem7  10527  ondomon  10575  cardmin  10576  alephval2  10584  alephreg  10594  smobeth  10598  winainflem  10705  inar1  10787  inatsk  10790  sltval2  27618  sltres  27624  nosepeq  27647  nosupno  27665  nosupres  27669  nosupbnd1lem1  27670  nosupbnd2lem1  27677  nosupbnd2  27678  noinfno  27680  noinfres  27684  noinfbnd1lem1  27685  noinfbnd2lem1  27692  noinfbnd2  27693  oldlim  27842  oldbday  27856  dfrdg2  35759  dfrdg4  35915  ontopbas  36392  onpsstopbas  36394  onint1  36413  onelord  43222  cantnfresb  43295  oawordex2  43297  oacl2g  43301  omabs2  43303  omcl2  43304  tfsconcatfv2  43311  tfsconcatfv  43312  tfsconcatrn  43313  tfsconcat0i  43316  ofoafg  43325  ofoaass  43331  oaun3lem1  43345  oaun3lem2  43346  oadif1lem  43350  oadif1  43351  nadd2rabtr  43355  nadd1suc  43363  naddgeoa  43365  naddwordnexlem0  43367  naddwordnexlem1  43368  naddwordnexlem3  43370  oawordex3  43371  naddwordnexlem4  43372  omssrncard  43511