Theorem onelon 6387

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366

This theorem is used by:  oneli  6478  ssorduni  7793  unon  7842  tfindsg2  7873  dfom2  7879  trom  7886  onfununi  8350  onnseq  8353  dfrecs3  8381  tz7.48-2  8453  tz7.49  8456  oalim  8541  omlim  8542  oelim  8543  oaordi  8555  oalimcl  8569  oaass  8570  omordi  8575  omlimcl  8587  odi  8588  omass  8589  omeulem1  8591  omeulem2  8592  omopth2  8593  oewordri  8602  oeordsuc  8604  oelimcl  8610  oeeui  8612  oaabs2  8659  omabs  8661  naddssim  8696  naddel12  8711  naddsuc2  8712  omxpenlem  9098  hartogs  9539  card2on  9549  cantnfle  9673  cantnflt  9674  cantnfp1lem3  9682  cantnfp1  9683  oemapvali  9686  cantnflem1b  9688  cantnflem1c  9689  cantnflem1d  9690  cantnflem1  9691  cantnflem2  9692  cantnflem3  9693  cantnflem4  9694  cantnf  9695  cnfcomlem  9701  cnfcom3lem  9705  cnfcom3  9706  r1ordg  9786  r1val3  9851  tskwe  10032  iscard  10057  cardmin2  10081  infxpenlem  10093  infxpenc2lem2  10100  alephordi  10154  alephord2i  10157  alephle  10168  cardaleph  10169  cfub  10327  cfsmolem  10349  zorn2lem5  10579  zorn2lem6  10580  ttukeylem6  10593  ttukeylem7  10594  ondomon  10648  cardmin  10649  alephval2  10658  alephreg  10668  smobeth  10672  winainflem  10779  inar1  10861  inatsk  10864  ltsval2  28014  ltsres  28020  nosepeq  28043  nosupno  28061  nosupres  28065  nosupbnd1lem1  28066  nosupbnd2lem1  28073  nosupbnd2  28074  noinfno  28076  noinfres  28080  noinfbnd1lem1  28081  noinfbnd2lem1  28088  noinfbnd2  28089  oldlim  28274  oldbday  28288  fineqvnttrclselem2  35839  dfrdg2  36632  dfrdg4  36790  nmulcom  37018  onelond  37023  nmuladdss  37037  nmulel1  37039  ltnmul  37040  nmulle  37041  ontopbas  37291  onpsstopbas  37293  onint1  37312  onelord  44329  cantnfresb  44402  oawordex2  44404  oacl2g  44408  omabs2  44410  omcl2  44411  tfsconcatfv2  44418  tfsconcatfv  44419  tfsconcatrn  44420  tfsconcat0i  44423  ofoafg  44432  ofoaass  44438  oaun3lem1  44452  oaun3lem2  44453  oadif1lem  44457  oadif1  44458  nadd2rabtr  44462  nadd1suc  44470  naddgeoa  44472  naddwordnexlem0  44474  naddwordnexlem1  44475  naddwordnexlem3  44477  oawordex3  44478  naddwordnexlem4  44479  omssrncard  44617