Theorem onelon 6332

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Ord word 6306  Oncon0 6307

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-tr 5200  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311

This theorem is referenced by:  oneli  6422  ssorduni  7715  unon  7764  tfindsg2  7795  dfom2  7801  trom  7808  onfununi  8264  onnseq  8267  dfrecs3  8295  tz7.48-2  8364  tz7.49  8367  oalim  8450  omlim  8451  oelim  8452  oaordi  8464  oalimcl  8478  oaass  8479  omordi  8484  omlimcl  8496  odi  8497  omass  8498  omeulem1  8500  omeulem2  8501  omopth2  8502  oewordri  8510  oeordsuc  8512  oelimcl  8518  oeeui  8520  oaabs2  8567  omabs  8569  naddssim  8603  naddel12  8618  naddsuc2  8619  omxpenlem  8995  hartogs  9436  card2on  9446  cantnfle  9567  cantnflt  9568  cantnfp1lem3  9576  cantnfp1  9577  oemapvali  9580  cantnflem1b  9582  cantnflem1c  9583  cantnflem1d  9584  cantnflem1  9585  cantnflem2  9586  cantnflem3  9587  cantnflem4  9588  cantnf  9589  cnfcomlem  9595  cnfcom3lem  9599  cnfcom3  9600  r1ordg  9674  r1val3  9734  tskwe  9846  iscard  9871  cardmin2  9895  infxpenlem  9907  infxpenc2lem2  9914  alephordi  9968  alephord2i  9971  alephle  9982  cardaleph  9983  cfub  10143  cfsmolem  10164  zorn2lem5  10394  zorn2lem6  10395  ttukeylem6  10408  ttukeylem7  10409  ondomon  10457  cardmin  10458  alephval2  10466  alephreg  10476  smobeth  10480  winainflem  10587  inar1  10669  inatsk  10672  sltval2  27566  sltres  27572  nosepeq  27595  nosupno  27613  nosupres  27617  nosupbnd1lem1  27618  nosupbnd2lem1  27625  nosupbnd2  27626  noinfno  27628  noinfres  27632  noinfbnd1lem1  27633  noinfbnd2lem1  27640  noinfbnd2  27641  oldlim  27803  oldbday  27817  fineqvnttrclselem2  35091  dfrdg2  35789  dfrdg4  35945  ontopbas  36422  onpsstopbas  36424  onint1  36443  onelord  43244  cantnfresb  43317  oawordex2  43319  oacl2g  43323  omabs2  43325  omcl2  43326  tfsconcatfv2  43333  tfsconcatfv  43334  tfsconcatrn  43335  tfsconcat0i  43338  ofoafg  43347  ofoaass  43353  oaun3lem1  43367  oaun3lem2  43368  oadif1lem  43372  oadif1  43373  nadd2rabtr  43377  nadd1suc  43385  naddgeoa  43387  naddwordnexlem0  43389  naddwordnexlem1  43390  naddwordnexlem3  43392  oawordex3  43393  naddwordnexlem4  43394  omssrncard  43533