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)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141  Ord word 6359  Oncon0 6360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3415  df-v 3455  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 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364

This theorem is referenced by:  oneli  6476  ssorduni  7777  unon  7826  tfindsg2  7857  dfom2  7863  trom  7870  onfununi  8327  onnseq  8330  dfrecs3  8358  tz7.48-2  8428  tz7.49  8431  oalim  8516  omlim  8517  oelim  8518  oaordi  8530  oalimcl  8544  oaass  8545  omordi  8550  omlimcl  8562  odi  8563  omass  8564  omeulem1  8566  omeulem2  8567  omopth2  8568  oewordri  8577  oeordsuc  8579  oelimcl  8585  oeeui  8587  oaabs2  8634  omabs  8636  naddssim  8671  naddel12  8686  naddsuc2  8687  omxpenlem  9065  hartogs  9505  card2on  9515  cantnfle  9639  cantnflt  9640  cantnfp1lem3  9648  cantnfp1  9649  oemapvali  9652  cantnflem1b  9654  cantnflem1c  9655  cantnflem1d  9656  cantnflem1  9657  cantnflem2  9658  cantnflem3  9659  cantnflem4  9660  cantnf  9661  cnfcomlem  9667  cnfcom3lem  9671  cnfcom3  9672  r1ordg  9749  r1val3  9809  tskwe  9935  iscard  9960  cardmin2  9984  infxpenlem  9996  infxpenc2lem2  10003  alephordi  10057  alephord2i  10060  alephle  10071  cardaleph  10072  cfub  10231  cfsmolem  10253  zorn2lem5  10483  zorn2lem6  10484  ttukeylem6  10497  ttukeylem7  10498  ondomon  10546  cardmin  10547  alephval2  10556  alephreg  10566  smobeth  10570  winainflem  10677  inar1  10759  inatsk  10762  ltsval2  27796  ltsres  27802  nosepeq  27825  nosupno  27843  nosupres  27847  nosupbnd1lem1  27848  nosupbnd2lem1  27855  nosupbnd2  27856  noinfno  27858  noinfres  27862  noinfbnd1lem1  27863  noinfbnd2lem1  27870  noinfbnd2  27871  oldlim  28056  oldbday  28070  fineqvnttrclselem2  35501  dfrdg2  36251  dfrdg4  36409  nmulcom  36652  nmuladdss  36656  nmulel1  36658  ltnmul  36659  nmulle  36660  ontopbas  36905  onpsstopbas  36907  onint1  36926  onelord  43948  cantnfresb  44021  oawordex2  44023  oacl2g  44027  omabs2  44029  omcl2  44030  tfsconcatfv2  44037  tfsconcatfv  44038  tfsconcatrn  44039  tfsconcat0i  44042  ofoafg  44051  ofoaass  44057  oaun3lem1  44071  oaun3lem2  44072  oadif1lem  44076  oadif1  44077  nadd2rabtr  44081  nadd1suc  44089  naddgeoa  44091  naddwordnexlem0  44093  naddwordnexlem1  44094  naddwordnexlem3  44096  oawordex3  44097  naddwordnexlem4  44098  omssrncard  44236