Theorem onelon 6342

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Ord word 6316  Oncon0 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5187  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321

This theorem is referenced by:  oneli  6432  ssorduni  7729  unon  7778  tfindsg2  7809  dfom2  7815  trom  7822  onfununi  8278  onnseq  8281  dfrecs3  8309  tz7.48-2  8378  tz7.49  8381  oalim  8464  omlim  8465  oelim  8466  oaordi  8478  oalimcl  8492  oaass  8493  omordi  8498  omlimcl  8510  odi  8511  omass  8512  omeulem1  8514  omeulem2  8515  omopth2  8516  oewordri  8525  oeordsuc  8527  oelimcl  8533  oeeui  8535  oaabs2  8582  omabs  8584  naddssim  8618  naddel12  8633  naddsuc2  8634  omxpenlem  9013  hartogs  9456  card2on  9466  cantnfle  9590  cantnflt  9591  cantnfp1lem3  9599  cantnfp1  9600  oemapvali  9603  cantnflem1b  9605  cantnflem1c  9606  cantnflem1d  9607  cantnflem1  9608  cantnflem2  9609  cantnflem3  9610  cantnflem4  9611  cantnf  9612  cnfcomlem  9618  cnfcom3lem  9622  cnfcom3  9623  r1ordg  9700  r1val3  9760  tskwe  9872  iscard  9897  cardmin2  9921  infxpenlem  9933  infxpenc2lem2  9940  alephordi  9994  alephord2i  9997  alephle  10008  cardaleph  10009  cfub  10169  cfsmolem  10190  zorn2lem5  10420  zorn2lem6  10421  ttukeylem6  10434  ttukeylem7  10435  ondomon  10483  cardmin  10484  alephval2  10493  alephreg  10503  smobeth  10507  winainflem  10614  inar1  10696  inatsk  10699  ltsval2  27645  ltsres  27651  nosepeq  27674  nosupno  27692  nosupres  27696  nosupbnd1lem1  27697  nosupbnd2lem1  27704  nosupbnd2  27705  noinfno  27707  noinfres  27711  noinfbnd1lem1  27712  noinfbnd2lem1  27719  noinfbnd2  27720  oldlim  27904  oldbday  27918  fineqvnttrclselem2  35313  dfrdg2  36022  dfrdg4  36180  ontopbas  36657  onpsstopbas  36659  onint1  36678  onelord  43697  cantnfresb  43770  oawordex2  43772  oacl2g  43776  omabs2  43778  omcl2  43779  tfsconcatfv2  43786  tfsconcatfv  43787  tfsconcatrn  43788  tfsconcat0i  43791  ofoafg  43800  ofoaass  43806  oaun3lem1  43820  oaun3lem2  43821  oadif1lem  43825  oadif1  43826  nadd2rabtr  43830  nadd1suc  43838  naddgeoa  43840  naddwordnexlem0  43842  naddwordnexlem1  43843  naddwordnexlem3  43845  oawordex3  43846  naddwordnexlem4  43847  omssrncard  43985