Theorem onelon 6340

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Ord word 6314  Oncon0 6315

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 5231  ax-pr 5368

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319

This theorem is referenced by:  oneli  6430  ssorduni  7724  unon  7773  tfindsg2  7804  dfom2  7810  trom  7817  onfununi  8272  onnseq  8275  dfrecs3  8303  tz7.48-2  8372  tz7.49  8375  oalim  8458  omlim  8459  oelim  8460  oaordi  8472  oalimcl  8486  oaass  8487  omordi  8492  omlimcl  8504  odi  8505  omass  8506  omeulem1  8508  omeulem2  8509  omopth2  8510  oewordri  8519  oeordsuc  8521  oelimcl  8527  oeeui  8529  oaabs2  8576  omabs  8578  naddssim  8612  naddel12  8627  naddsuc2  8628  omxpenlem  9007  hartogs  9450  card2on  9460  cantnfle  9581  cantnflt  9582  cantnfp1lem3  9590  cantnfp1  9591  oemapvali  9594  cantnflem1b  9596  cantnflem1c  9597  cantnflem1d  9598  cantnflem1  9599  cantnflem2  9600  cantnflem3  9601  cantnflem4  9602  cantnf  9603  cnfcomlem  9609  cnfcom3lem  9613  cnfcom3  9614  r1ordg  9691  r1val3  9751  tskwe  9863  iscard  9888  cardmin2  9912  infxpenlem  9924  infxpenc2lem2  9931  alephordi  9985  alephord2i  9988  alephle  9999  cardaleph  10000  cfub  10160  cfsmolem  10181  zorn2lem5  10411  zorn2lem6  10412  ttukeylem6  10425  ttukeylem7  10426  ondomon  10474  cardmin  10475  alephval2  10484  alephreg  10494  smobeth  10498  winainflem  10605  inar1  10687  inatsk  10690  ltsval2  27639  ltsres  27645  nosepeq  27668  nosupno  27686  nosupres  27690  nosupbnd1lem1  27691  nosupbnd2lem1  27698  nosupbnd2  27699  noinfno  27701  noinfres  27705  noinfbnd1lem1  27706  noinfbnd2lem1  27713  noinfbnd2  27714  oldlim  27898  oldbday  27912  fineqvnttrclselem2  35287  dfrdg2  35996  dfrdg4  36154  ontopbas  36631  onpsstopbas  36633  onint1  36652  onelord  43694  cantnfresb  43767  oawordex2  43769  oacl2g  43773  omabs2  43775  omcl2  43776  tfsconcatfv2  43783  tfsconcatfv  43784  tfsconcatrn  43785  tfsconcat0i  43788  ofoafg  43797  ofoaass  43803  oaun3lem1  43817  oaun3lem2  43818  oadif1lem  43822  oadif1  43823  nadd2rabtr  43827  nadd1suc  43835  naddgeoa  43837  naddwordnexlem0  43839  naddwordnexlem1  43840  naddwordnexlem3  43842  oawordex3  43843  naddwordnexlem4  43844  omssrncard  43982