Theorem onelon 6350

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Ord word 6324  Oncon0 6325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329

This theorem is referenced by:  oneli  6440  ssorduni  7734  unon  7783  tfindsg2  7814  dfom2  7820  trom  7827  onfununi  8283  onnseq  8286  dfrecs3  8314  tz7.48-2  8383  tz7.49  8386  oalim  8469  omlim  8470  oelim  8471  oaordi  8483  oalimcl  8497  oaass  8498  omordi  8503  omlimcl  8515  odi  8516  omass  8517  omeulem1  8519  omeulem2  8520  omopth2  8521  oewordri  8530  oeordsuc  8532  oelimcl  8538  oeeui  8540  oaabs2  8587  omabs  8589  naddssim  8623  naddel12  8638  naddsuc2  8639  omxpenlem  9018  hartogs  9461  card2on  9471  cantnfle  9592  cantnflt  9593  cantnfp1lem3  9601  cantnfp1  9602  oemapvali  9605  cantnflem1b  9607  cantnflem1c  9608  cantnflem1d  9609  cantnflem1  9610  cantnflem2  9611  cantnflem3  9612  cantnflem4  9613  cantnf  9614  cnfcomlem  9620  cnfcom3lem  9624  cnfcom3  9625  r1ordg  9702  r1val3  9762  tskwe  9874  iscard  9899  cardmin2  9923  infxpenlem  9935  infxpenc2lem2  9942  alephordi  9996  alephord2i  9999  alephle  10010  cardaleph  10011  cfub  10171  cfsmolem  10192  zorn2lem5  10422  zorn2lem6  10423  ttukeylem6  10436  ttukeylem7  10437  ondomon  10485  cardmin  10486  alephval2  10495  alephreg  10505  smobeth  10509  winainflem  10616  inar1  10698  inatsk  10701  ltsval2  27636  ltsres  27642  nosepeq  27665  nosupno  27683  nosupres  27687  nosupbnd1lem1  27688  nosupbnd2lem1  27695  nosupbnd2  27696  noinfno  27698  noinfres  27702  noinfbnd1lem1  27703  noinfbnd2lem1  27710  noinfbnd2  27711  oldlim  27895  oldbday  27909  fineqvnttrclselem2  35297  dfrdg2  36006  dfrdg4  36164  ontopbas  36641  onpsstopbas  36643  onint1  36662  onelord  43597  cantnfresb  43670  oawordex2  43672  oacl2g  43676  omabs2  43678  omcl2  43679  tfsconcatfv2  43686  tfsconcatfv  43687  tfsconcatrn  43688  tfsconcat0i  43691  ofoafg  43700  ofoaass  43706  oaun3lem1  43720  oaun3lem2  43721  oadif1lem  43725  oadif1  43726  nadd2rabtr  43730  nadd1suc  43738  naddgeoa  43740  naddwordnexlem0  43742  naddwordnexlem1  43743  naddwordnexlem3  43745  oawordex3  43746  naddwordnexlem4  43747  omssrncard  43885