Theorem onelon 5889

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

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 2145  Ord word 5863  Oncon0 5864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-tr 4887  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5867  df-on 5868

This theorem is referenced by:  oneli  5976  ssorduni  7132  unon  7178  tfindsg2  7208  dfom2  7214  ordom  7221  onfununi  7591  onnseq  7594  dfrecs3  7622  tz7.48-2  7690  tz7.49  7693  oalim  7766  omlim  7767  oelim  7768  oaordi  7780  oalimcl  7794  oaass  7795  omordi  7800  omlimcl  7812  odi  7813  omass  7814  omeulem1  7816  omeulem2  7817  omopth2  7818  oewordri  7826  oeordsuc  7828  oelimcl  7834  oeeui  7836  oaabs2  7879  omabs  7881  omxpenlem  8217  hartogs  8605  card2on  8615  cantnfle  8732  cantnflt  8733  cantnfp1lem2  8740  cantnfp1lem3  8741  cantnfp1  8742  oemapvali  8745  cantnflem1b  8747  cantnflem1c  8748  cantnflem1d  8749  cantnflem1  8750  cantnflem2  8751  cantnflem3  8752  cantnflem4  8753  cantnf  8754  cnfcomlem  8760  cnfcom3lem  8764  cnfcom3  8765  r1ordg  8805  r1val3  8865  tskwe  8976  iscard  9001  cardmin2  9024  infxpenlem  9036  infxpenc2lem2  9043  alephordi  9097  alephord2i  9100  alephle  9111  cardaleph  9112  cfub  9273  cfsmolem  9294  zorn2lem5  9524  zorn2lem6  9525  ttukeylem6  9538  ttukeylem7  9539  ondomon  9587  cardmin  9588  alephval2  9596  alephreg  9606  smobeth  9610  winainflem  9717  inar1  9799  inatsk  9802  dfrdg2  32033  sltval2  32142  sltres  32148  nosepeq  32168  nosupno  32182  nosupres  32186  nosupbnd1lem1  32187  nosupbnd2lem1  32194  nosupbnd2  32195  dfrdg4  32391  ontopbas  32760  onpsstopbas  32762  onint1  32781