Theorem onelon 6360

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2136  Ord word 6334  Oncon0 6335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-sep 5240  ax-pr 5384

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-tr 5202  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-we 5595  df-ord 6338  df-on 6339

This theorem is referenced by:  oneli  6450  ssorduni  7751  unon  7800  tfindsg2  7831  dfom2  7837  trom  7844  onfununi  8300  onnseq  8303  dfrecs3  8331  tz7.48-2  8401  tz7.49  8404  oalim  8489  omlim  8490  oelim  8491  oaordi  8503  oalimcl  8517  oaass  8518  omordi  8523  omlimcl  8535  odi  8536  omass  8537  omeulem1  8539  omeulem2  8540  omopth2  8541  oewordri  8550  oeordsuc  8552  oelimcl  8558  oeeui  8560  oaabs2  8607  omabs  8609  naddssim  8644  naddel12  8659  naddsuc2  8660  omxpenlem  9039  hartogs  9482  card2on  9492  cantnfle  9616  cantnflt  9617  cantnfp1lem3  9625  cantnfp1  9626  oemapvali  9629  cantnflem1b  9631  cantnflem1c  9632  cantnflem1d  9633  cantnflem1  9634  cantnflem2  9635  cantnflem3  9636  cantnflem4  9637  cantnf  9638  cnfcomlem  9644  cnfcom3lem  9648  cnfcom3  9649  r1ordg  9726  r1val3  9786  tskwe  9898  iscard  9923  cardmin2  9947  infxpenlem  9959  infxpenc2lem2  9966  alephordi  10020  alephord2i  10023  alephle  10034  cardaleph  10035  cfub  10195  cfsmolem  10217  zorn2lem5  10447  zorn2lem6  10448  ttukeylem6  10461  ttukeylem7  10462  ondomon  10510  cardmin  10511  alephval2  10520  alephreg  10530  smobeth  10534  winainflem  10641  inar1  10723  inatsk  10726  ltsval2  27690  ltsres  27696  nosepeq  27719  nosupno  27737  nosupres  27741  nosupbnd1lem1  27742  nosupbnd2lem1  27749  nosupbnd2  27750  noinfno  27752  noinfres  27756  noinfbnd1lem1  27757  noinfbnd2lem1  27764  noinfbnd2  27765  oldlim  27950  oldbday  27964  fineqvnttrclselem2  35373  dfrdg2  36091  dfrdg4  36249  nmulcom  36492  ontopbas  36736  onpsstopbas  36738  onint1  36757  onelord  43776  cantnfresb  43849  oawordex2  43851  oacl2g  43855  omabs2  43857  omcl2  43858  tfsconcatfv2  43865  tfsconcatfv  43866  tfsconcatrn  43867  tfsconcat0i  43870  ofoafg  43879  ofoaass  43885  oaun3lem1  43899  oaun3lem2  43900  oadif1lem  43904  oadif1  43905  nadd2rabtr  43909  nadd1suc  43917  naddgeoa  43919  naddwordnexlem0  43921  naddwordnexlem1  43922  naddwordnexlem3  43924  oawordex3  43925  naddwordnexlem4  43926  omssrncard  44064