Theorem onelon 6360

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Ord word 6334  Oncon0 6335

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339

This theorem is referenced by:  oneli  6451  ssorduni  7758  unon  7809  tfindsg2  7841  dfom2  7847  trom  7854  onfununi  8313  onnseq  8316  dfrecs3  8344  tz7.48-2  8413  tz7.49  8416  oalim  8499  omlim  8500  oelim  8501  oaordi  8513  oalimcl  8527  oaass  8528  omordi  8533  omlimcl  8545  odi  8546  omass  8547  omeulem1  8549  omeulem2  8550  omopth2  8551  oewordri  8559  oeordsuc  8561  oelimcl  8567  oeeui  8569  oaabs2  8616  omabs  8618  naddssim  8652  naddel12  8667  naddsuc2  8668  omxpenlem  9047  hartogs  9504  card2on  9514  cantnfle  9631  cantnflt  9632  cantnfp1lem3  9640  cantnfp1  9641  oemapvali  9644  cantnflem1b  9646  cantnflem1c  9647  cantnflem1d  9648  cantnflem1  9649  cantnflem2  9650  cantnflem3  9651  cantnflem4  9652  cantnf  9653  cnfcomlem  9659  cnfcom3lem  9663  cnfcom3  9664  r1ordg  9738  r1val3  9798  tskwe  9910  iscard  9935  cardmin2  9959  infxpenlem  9973  infxpenc2lem2  9980  alephordi  10034  alephord2i  10037  alephle  10048  cardaleph  10049  cfub  10209  cfsmolem  10230  zorn2lem5  10460  zorn2lem6  10461  ttukeylem6  10474  ttukeylem7  10475  ondomon  10523  cardmin  10524  alephval2  10532  alephreg  10542  smobeth  10546  winainflem  10653  inar1  10735  inatsk  10738  sltval2  27575  sltres  27581  nosepeq  27604  nosupno  27622  nosupres  27626  nosupbnd1lem1  27627  nosupbnd2lem1  27634  nosupbnd2  27635  noinfno  27637  noinfres  27641  noinfbnd1lem1  27642  noinfbnd2lem1  27649  noinfbnd2  27650  oldlim  27805  oldbday  27819  dfrdg2  35790  dfrdg4  35946  ontopbas  36423  onpsstopbas  36425  onint1  36444  onelord  43247  cantnfresb  43320  oawordex2  43322  oacl2g  43326  omabs2  43328  omcl2  43329  tfsconcatfv2  43336  tfsconcatfv  43337  tfsconcatrn  43338  tfsconcat0i  43341  ofoafg  43350  ofoaass  43356  oaun3lem1  43370  oaun3lem2  43371  oadif1lem  43375  oadif1  43376  nadd2rabtr  43380  nadd1suc  43388  naddgeoa  43390  naddwordnexlem0  43392  naddwordnexlem1  43393  naddwordnexlem3  43395  oawordex3  43396  naddwordnexlem4  43397  omssrncard  43536