Theorem onelon 5958

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 2158  Ord word 5932  Oncon0 5933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pr 5093

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-rab 3104  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4627  df-br 4841  df-opab 4903  df-tr 4943  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-ord 5936  df-on 5937

This theorem is referenced by:  oneli  6045  ssorduni  7212  unon  7258  tfindsg2  7288  dfom2  7294  ordom  7301  onfununi  7671  onnseq  7674  dfrecs3  7702  tz7.48-2  7770  tz7.49  7773  oalim  7846  omlim  7847  oelim  7848  oaordi  7860  oalimcl  7874  oaass  7875  omordi  7880  omlimcl  7892  odi  7893  omass  7894  omeulem1  7896  omeulem2  7897  omopth2  7898  oewordri  7906  oeordsuc  7908  oelimcl  7914  oeeui  7916  oaabs2  7959  omabs  7961  omxpenlem  8297  hartogs  8685  card2on  8695  cantnfle  8812  cantnflt  8813  cantnfp1lem2  8820  cantnfp1lem3  8821  cantnfp1  8822  oemapvali  8825  cantnflem1b  8827  cantnflem1c  8828  cantnflem1d  8829  cantnflem1  8830  cantnflem2  8831  cantnflem3  8832  cantnflem4  8833  cantnf  8834  cnfcomlem  8840  cnfcom3lem  8844  cnfcom3  8845  r1ordg  8885  r1val3  8945  tskwe  9056  iscard  9081  cardmin2  9104  infxpenlem  9116  infxpenc2lem2  9123  alephordi  9177  alephord2i  9180  alephle  9191  cardaleph  9192  cfub  9353  cfsmolem  9374  zorn2lem5  9604  zorn2lem6  9605  ttukeylem6  9618  ttukeylem7  9619  ondomon  9667  cardmin  9668  alephval2  9676  alephreg  9686  smobeth  9690  winainflem  9797  inar1  9879  inatsk  9882  dfrdg2  32018  sltval2  32127  sltres  32133  nosepeq  32153  nosupno  32167  nosupres  32171  nosupbnd1lem1  32172  nosupbnd2lem1  32179  nosupbnd2  32180  dfrdg4  32376  ontopbas  32741  onpsstopbas  32743  onint1  32762