Theorem onelon 6390

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  Ord word 6364  Oncon0 6365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369

This theorem is referenced by:  oneli  6479  ssorduni  7766  unon  7819  tfindsg2  7851  dfom2  7857  trom  7864  onfununi  8341  onnseq  8344  dfrecs3  8372  dfrecs3OLD  8373  tz7.48-2  8442  tz7.49  8445  oalim  8532  omlim  8533  oelim  8534  oaordi  8546  oalimcl  8560  oaass  8561  omordi  8566  omlimcl  8578  odi  8579  omass  8580  omeulem1  8582  omeulem2  8583  omopth2  8584  oewordri  8592  oeordsuc  8594  oelimcl  8600  oeeui  8602  oaabs2  8648  omabs  8650  naddssim  8684  naddel12  8699  omxpenlem  9073  hartogs  9539  card2on  9549  cantnfle  9666  cantnflt  9667  cantnfp1lem3  9675  cantnfp1  9676  oemapvali  9679  cantnflem1b  9681  cantnflem1c  9682  cantnflem1d  9683  cantnflem1  9684  cantnflem2  9685  cantnflem3  9686  cantnflem4  9687  cantnf  9688  cnfcomlem  9694  cnfcom3lem  9698  cnfcom3  9699  r1ordg  9773  r1val3  9833  tskwe  9945  iscard  9970  cardmin2  9994  infxpenlem  10008  infxpenc2lem2  10015  alephordi  10069  alephord2i  10072  alephle  10083  cardaleph  10084  cfub  10244  cfsmolem  10265  zorn2lem5  10495  zorn2lem6  10496  ttukeylem6  10509  ttukeylem7  10510  ondomon  10558  cardmin  10559  alephval2  10567  alephreg  10577  smobeth  10581  winainflem  10688  inar1  10770  inatsk  10773  sltval2  27159  sltres  27165  nosepeq  27188  nosupno  27206  nosupres  27210  nosupbnd1lem1  27211  nosupbnd2lem1  27218  nosupbnd2  27219  noinfno  27221  noinfres  27225  noinfbnd1lem1  27226  noinfbnd2lem1  27233  noinfbnd2  27234  oldlim  27382  oldbday  27396  dfrdg2  34798  dfrdg4  34954  ontopbas  35361  onpsstopbas  35363  onint1  35382  onelord  42048  cantnfresb  42122  oawordex2  42124  oacl2g  42128  omabs2  42130  omcl2  42131  tfsconcatfv2  42138  tfsconcatfv  42139  tfsconcatrn  42140  tfsconcat0i  42143  ofoafg  42152  ofoaass  42158  oaun3lem1  42172  oaun3lem2  42173  oadif1lem  42177  oadif1  42178  nadd2rabtr  42182  nadd1suc  42190  naddsuc2  42191  naddgeoa  42193  naddwordnexlem0  42195  naddwordnexlem1  42196  naddwordnexlem3  42198  oawordex3  42199  naddwordnexlem4  42200  omssrncard  42339