Theorem onelon 6216

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  Ord word 6190  Oncon0 6191

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-tr 5173  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-ord 6194  df-on 6195

This theorem is referenced by:  oneli  6298  ssorduni  7500  unon  7546  tfindsg2  7576  dfom2  7582  ordom  7589  onfununi  7978  onnseq  7981  dfrecs3  8009  tz7.48-2  8078  tz7.49  8081  oalim  8157  omlim  8158  oelim  8159  oaordi  8172  oalimcl  8186  oaass  8187  omordi  8192  omlimcl  8204  odi  8205  omass  8206  omeulem1  8208  omeulem2  8209  omopth2  8210  oewordri  8218  oeordsuc  8220  oelimcl  8226  oeeui  8228  oaabs2  8272  omabs  8274  omxpenlem  8618  hartogs  9008  card2on  9018  cantnfle  9134  cantnflt  9135  cantnfp1lem3  9143  cantnfp1  9144  oemapvali  9147  cantnflem1b  9149  cantnflem1c  9150  cantnflem1d  9151  cantnflem1  9152  cantnflem2  9153  cantnflem3  9154  cantnflem4  9155  cantnf  9156  cnfcomlem  9162  cnfcom3lem  9166  cnfcom3  9167  r1ordg  9207  r1val3  9267  tskwe  9379  iscard  9404  cardmin2  9427  infxpenlem  9439  infxpenc2lem2  9446  alephordi  9500  alephord2i  9503  alephle  9514  cardaleph  9515  cfub  9671  cfsmolem  9692  zorn2lem5  9922  zorn2lem6  9923  ttukeylem6  9936  ttukeylem7  9937  ondomon  9985  cardmin  9986  alephval2  9994  alephreg  10004  smobeth  10008  winainflem  10115  inar1  10197  inatsk  10200  dfrdg2  33040  sltval2  33163  sltres  33169  nosepeq  33189  nosupno  33203  nosupres  33207  nosupbnd1lem1  33208  nosupbnd2lem1  33215  nosupbnd2  33216  dfrdg4  33412  ontopbas  33776  onpsstopbas  33778  onint1  33797