Theorem onelon 6349

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

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

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 5232  ax-pr 5376

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 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6327  df-on 6328

This theorem is referenced by:  oneli  6439  ssorduni  7733  unon  7782  tfindsg2  7813  dfom2  7819  trom  7826  onfununi  8281  onnseq  8284  dfrecs3  8312  tz7.48-2  8381  tz7.49  8384  oalim  8467  omlim  8468  oelim  8469  oaordi  8481  oalimcl  8495  oaass  8496  omordi  8501  omlimcl  8513  odi  8514  omass  8515  omeulem1  8517  omeulem2  8518  omopth2  8519  oewordri  8528  oeordsuc  8530  oelimcl  8536  oeeui  8538  oaabs2  8585  omabs  8587  naddssim  8621  naddel12  8636  naddsuc2  8637  omxpenlem  9016  hartogs  9459  card2on  9469  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  27620  ltsres  27626  nosepeq  27649  nosupno  27667  nosupres  27671  nosupbnd1lem1  27672  nosupbnd2lem1  27679  nosupbnd2  27680  noinfno  27682  noinfres  27686  noinfbnd1lem1  27687  noinfbnd2lem1  27694  noinfbnd2  27695  oldlim  27879  oldbday  27893  fineqvnttrclselem2  35266  dfrdg2  35975  dfrdg4  36133  ontopbas  36610  onpsstopbas  36612  onint1  36631  onelord  43679  cantnfresb  43752  oawordex2  43754  oacl2g  43758  omabs2  43760  omcl2  43761  tfsconcatfv2  43768  tfsconcatfv  43769  tfsconcatrn  43770  tfsconcat0i  43773  ofoafg  43782  ofoaass  43788  oaun3lem1  43802  oaun3lem2  43803  oadif1lem  43807  oadif1  43808  nadd2rabtr  43812  nadd1suc  43820  naddgeoa  43822  naddwordnexlem0  43824  naddwordnexlem1  43825  naddwordnexlem3  43827  oawordex3  43828  naddwordnexlem4  43829  omssrncard  43967