Theorem onelon 6238

Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)

Assertion

Ref	Expression
onelon	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Proof of Theorem onelon

Step	Hyp	Ref	Expression
1		eloni 6223	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelon 6237	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
3	1, 2	sylan 583	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  Ord word 6212  Oncon0 6213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-11 2158  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3066  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-tr 5162  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-ord 6216  df-on 6217

This theorem is referenced by:  oneli  6321  ssorduni  7563  unon  7610  tfindsg2  7640  dfom2  7646  trom  7653  onfununi  8078  onnseq  8081  dfrecs3  8109  tz7.48-2  8178  tz7.49  8181  oalim  8259  omlim  8260  oelim  8261  oaordi  8274  oalimcl  8288  oaass  8289  omordi  8294  omlimcl  8306  odi  8307  omass  8308  omeulem1  8310  omeulem2  8311  omopth2  8312  oewordri  8320  oeordsuc  8322  oelimcl  8328  oeeui  8330  oaabs2  8374  omabs  8376  omxpenlem  8746  hartogs  9160  card2on  9170  cantnfle  9286  cantnflt  9287  cantnfp1lem3  9295  cantnfp1  9296  oemapvali  9299  cantnflem1b  9301  cantnflem1c  9302  cantnflem1d  9303  cantnflem1  9304  cantnflem2  9305  cantnflem3  9306  cantnflem4  9307  cantnf  9308  cnfcomlem  9314  cnfcom3lem  9318  cnfcom3  9319  r1ordg  9394  r1val3  9454  tskwe  9566  iscard  9591  cardmin2  9615  infxpenlem  9627  infxpenc2lem2  9634  alephordi  9688  alephord2i  9691  alephle  9702  cardaleph  9703  cfub  9863  cfsmolem  9884  zorn2lem5  10114  zorn2lem6  10115  ttukeylem6  10128  ttukeylem7  10129  ondomon  10177  cardmin  10178  alephval2  10186  alephreg  10196  smobeth  10200  winainflem  10307  inar1  10389  inatsk  10392  dfrdg2  33490  naddssim  33574  sltval2  33596  sltres  33602  nosepeq  33625  nosupno  33643  nosupres  33647  nosupbnd1lem1  33648  nosupbnd2lem1  33655  nosupbnd2  33656  noinfno  33658  noinfres  33662  noinfbnd1lem1  33663  noinfbnd2lem1  33670  noinfbnd2  33671  oldlim  33806  oldbday  33818  dfrdg4  33990  ontopbas  34354  onpsstopbas  34356  onint1  34375