Theorem onelon 6327

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2110  Ord word 6301  Oncon0 6302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-tr 5197  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6305  df-on 6306

This theorem is referenced by:  oneli  6417  ssorduni  7707  unon  7756  tfindsg2  7787  dfom2  7793  trom  7800  onfununi  8256  onnseq  8259  dfrecs3  8287  tz7.48-2  8356  tz7.49  8359  oalim  8442  omlim  8443  oelim  8444  oaordi  8456  oalimcl  8470  oaass  8471  omordi  8476  omlimcl  8488  odi  8489  omass  8490  omeulem1  8492  omeulem2  8493  omopth2  8494  oewordri  8502  oeordsuc  8504  oelimcl  8510  oeeui  8512  oaabs2  8559  omabs  8561  naddssim  8595  naddel12  8610  naddsuc2  8611  omxpenlem  8986  hartogs  9425  card2on  9435  cantnfle  9556  cantnflt  9557  cantnfp1lem3  9565  cantnfp1  9566  oemapvali  9569  cantnflem1b  9571  cantnflem1c  9572  cantnflem1d  9573  cantnflem1  9574  cantnflem2  9575  cantnflem3  9576  cantnflem4  9577  cantnf  9578  cnfcomlem  9584  cnfcom3lem  9588  cnfcom3  9589  r1ordg  9663  r1val3  9723  tskwe  9835  iscard  9860  cardmin2  9884  infxpenlem  9896  infxpenc2lem2  9903  alephordi  9957  alephord2i  9960  alephle  9971  cardaleph  9972  cfub  10132  cfsmolem  10153  zorn2lem5  10383  zorn2lem6  10384  ttukeylem6  10397  ttukeylem7  10398  ondomon  10446  cardmin  10447  alephval2  10455  alephreg  10465  smobeth  10469  winainflem  10576  inar1  10658  inatsk  10661  sltval2  27588  sltres  27594  nosepeq  27617  nosupno  27635  nosupres  27639  nosupbnd1lem1  27640  nosupbnd2lem1  27647  nosupbnd2  27648  noinfno  27650  noinfres  27654  noinfbnd1lem1  27655  noinfbnd2lem1  27662  noinfbnd2  27663  oldlim  27825  oldbday  27839  fineqvnttrclselem2  35110  dfrdg2  35808  dfrdg4  35964  ontopbas  36441  onpsstopbas  36443  onint1  36462  onelord  43263  cantnfresb  43336  oawordex2  43338  oacl2g  43342  omabs2  43344  omcl2  43345  tfsconcatfv2  43352  tfsconcatfv  43353  tfsconcatrn  43354  tfsconcat0i  43357  ofoafg  43366  ofoaass  43372  oaun3lem1  43386  oaun3lem2  43387  oadif1lem  43391  oadif1  43392  nadd2rabtr  43396  nadd1suc  43404  naddgeoa  43406  naddwordnexlem0  43408  naddwordnexlem1  43409  naddwordnexlem3  43411  oawordex3  43412  naddwordnexlem4  43413  omssrncard  43552