Theorem onelon 6291

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Ord word 6265  Oncon0 6266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270

This theorem is referenced by:  oneli  6374  ssorduni  7629  unon  7678  tfindsg2  7708  dfom2  7714  trom  7721  onfununi  8172  onnseq  8175  dfrecs3  8203  dfrecs3OLD  8204  tz7.48-2  8273  tz7.49  8276  oalim  8362  omlim  8363  oelim  8364  oaordi  8377  oalimcl  8391  oaass  8392  omordi  8397  omlimcl  8409  odi  8410  omass  8411  omeulem1  8413  omeulem2  8414  omopth2  8415  oewordri  8423  oeordsuc  8425  oelimcl  8431  oeeui  8433  oaabs2  8479  omabs  8481  omxpenlem  8860  hartogs  9303  card2on  9313  cantnfle  9429  cantnflt  9430  cantnfp1lem3  9438  cantnfp1  9439  oemapvali  9442  cantnflem1b  9444  cantnflem1c  9445  cantnflem1d  9446  cantnflem1  9447  cantnflem2  9448  cantnflem3  9449  cantnflem4  9450  cantnf  9451  cnfcomlem  9457  cnfcom3lem  9461  cnfcom3  9462  r1ordg  9536  r1val3  9596  tskwe  9708  iscard  9733  cardmin2  9757  infxpenlem  9769  infxpenc2lem2  9776  alephordi  9830  alephord2i  9833  alephle  9844  cardaleph  9845  cfub  10005  cfsmolem  10026  zorn2lem5  10256  zorn2lem6  10257  ttukeylem6  10270  ttukeylem7  10271  ondomon  10319  cardmin  10320  alephval2  10328  alephreg  10338  smobeth  10342  winainflem  10449  inar1  10531  inatsk  10534  dfrdg2  33771  naddssim  33837  sltval2  33859  sltres  33865  nosepeq  33888  nosupno  33906  nosupres  33910  nosupbnd1lem1  33911  nosupbnd2lem1  33918  nosupbnd2  33919  noinfno  33921  noinfres  33925  noinfbnd1lem1  33926  noinfbnd2lem1  33933  noinfbnd2  33934  oldlim  34069  oldbday  34081  dfrdg4  34253  ontopbas  34617  onpsstopbas  34619  onint1  34638  omssrncard  41147