Theorem onelon 6385

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142  Ord word 6359  Oncon0 6360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-tr 5218  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-ord 6363  df-on 6364

This theorem is used by:  oneli  6476  ssorduni  7776  unon  7825  tfindsg2  7856  dfom2  7862  trom  7869  onfununi  8326  onnseq  8329  dfrecs3  8357  tz7.48-2  8427  tz7.49  8430  oalim  8515  omlim  8516  oelim  8517  oaordi  8529  oalimcl  8543  oaass  8544  omordi  8549  omlimcl  8561  odi  8562  omass  8563  omeulem1  8565  omeulem2  8566  omopth2  8567  oewordri  8576  oeordsuc  8578  oelimcl  8584  oeeui  8586  oaabs2  8633  omabs  8635  naddssim  8670  naddel12  8685  naddsuc2  8686  omxpenlem  9064  hartogs  9504  card2on  9514  cantnfle  9638  cantnflt  9639  cantnfp1lem3  9647  cantnfp1  9648  oemapvali  9651  cantnflem1b  9653  cantnflem1c  9654  cantnflem1d  9655  cantnflem1  9656  cantnflem2  9657  cantnflem3  9658  cantnflem4  9659  cantnf  9660  cnfcomlem  9666  cnfcom3lem  9670  cnfcom3  9671  r1ordg  9748  r1val3  9808  tskwe  9943  iscard  9968  cardmin2  9992  infxpenlem  10004  infxpenc2lem2  10011  alephordi  10065  alephord2i  10068  alephle  10079  cardaleph  10080  cfub  10238  cfsmolem  10260  zorn2lem5  10490  zorn2lem6  10491  ttukeylem6  10504  ttukeylem7  10505  ondomon  10553  cardmin  10554  alephval2  10563  alephreg  10573  smobeth  10577  winainflem  10684  inar1  10766  inatsk  10769  ltsval2  27831  ltsres  27837  nosepeq  27860  nosupno  27878  nosupres  27882  nosupbnd1lem1  27883  nosupbnd2lem1  27890  nosupbnd2  27891  noinfno  27893  noinfres  27897  noinfbnd1lem1  27898  noinfbnd2lem1  27905  noinfbnd2  27906  oldlim  28091  oldbday  28105  fineqvnttrclselem2  35543  dfrdg2  36293  dfrdg4  36451  nmulcom  36694  onelond  36699  nmuladdss  36713  nmulel1  36715  ltnmul  36716  nmulle  36717  ontopbas  36967  onpsstopbas  36969  onint1  36988  onelord  44006  cantnfresb  44079  oawordex2  44081  oacl2g  44085  omabs2  44087  omcl2  44088  tfsconcatfv2  44095  tfsconcatfv  44096  tfsconcatrn  44097  tfsconcat0i  44100  ofoafg  44109  ofoaass  44115  oaun3lem1  44129  oaun3lem2  44130  oadif1lem  44134  oadif1  44135  nadd2rabtr  44139  nadd1suc  44147  naddgeoa  44149  naddwordnexlem0  44151  naddwordnexlem1  44152  naddwordnexlem3  44154  oawordex3  44155  naddwordnexlem4  44156  omssrncard  44294