Theorem onelon 6386

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

Assertion

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

Proof of Theorem onelon

Step	Hyp	Ref	Expression
1		eloni 6371	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		ordelon 6385	. 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
3	1, 2	sylan 592	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Ord word 6360  Oncon0 6361

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365

This theorem is used by:  oneli  6477  ssorduni  7781  unon  7830  tfindsg2  7861  dfom2  7867  trom  7874  onfununi  8333  onnseq  8336  dfrecs3  8364  tz7.48-2  8434  tz7.49  8437  oalim  8522  omlim  8523  oelim  8524  oaordi  8536  oalimcl  8550  oaass  8551  omordi  8556  omlimcl  8568  odi  8569  omass  8570  omeulem1  8572  omeulem2  8573  omopth2  8574  oewordri  8583  oeordsuc  8585  oelimcl  8591  oeeui  8593  oaabs2  8640  omabs  8642  naddssim  8677  naddel12  8692  naddsuc2  8693  omxpenlem  9079  hartogs  9519  card2on  9529  cantnfle  9653  cantnflt  9654  cantnfp1lem3  9662  cantnfp1  9663  oemapvali  9666  cantnflem1b  9668  cantnflem1c  9669  cantnflem1d  9670  cantnflem1  9671  cantnflem2  9672  cantnflem3  9673  cantnflem4  9674  cantnf  9675  cnfcomlem  9681  cnfcom3lem  9685  cnfcom3  9686  r1ordg  9763  r1val3  9823  tskwe  9958  iscard  9983  cardmin2  10007  infxpenlem  10019  infxpenc2lem2  10026  alephordi  10080  alephord2i  10083  alephle  10094  cardaleph  10095  cfub  10253  cfsmolem  10275  zorn2lem5  10505  zorn2lem6  10506  ttukeylem6  10519  ttukeylem7  10520  ondomon  10574  cardmin  10575  alephval2  10584  alephreg  10594  smobeth  10598  winainflem  10705  inar1  10787  inatsk  10790  ltsval2  27893  ltsres  27899  nosepeq  27922  nosupno  27940  nosupres  27944  nosupbnd1lem1  27945  nosupbnd2lem1  27952  nosupbnd2  27953  noinfno  27955  noinfres  27959  noinfbnd1lem1  27960  noinfbnd2lem1  27967  noinfbnd2  27968  oldlim  28153  oldbday  28167  fineqvnttrclselem2  35650  dfrdg2  36374  dfrdg4  36532  nmulcom  36776  onelond  36781  nmuladdss  36795  nmulel1  36797  ltnmul  36798  nmulle  36799  ontopbas  37049  onpsstopbas  37051  onint1  37070  onelord  44094  cantnfresb  44167  oawordex2  44169  oacl2g  44173  omabs2  44175  omcl2  44176  tfsconcatfv2  44183  tfsconcatfv  44184  tfsconcatrn  44185  tfsconcat0i  44188  ofoafg  44197  ofoaass  44203  oaun3lem1  44217  oaun3lem2  44218  oadif1lem  44222  oadif1  44223  nadd2rabtr  44227  nadd1suc  44235  naddgeoa  44237  naddwordnexlem0  44239  naddwordnexlem1  44240  naddwordnexlem3  44242  oawordex3  44243  naddwordnexlem4  44244  omssrncard  44382