Theorem onelon 6339

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Ord word 6313  Oncon0 6314

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318

This theorem is referenced by:  oneli  6429  ssorduni  7721  unon  7770  tfindsg2  7801  dfom2  7807  trom  7814  onfununi  8270  onnseq  8273  dfrecs3  8301  tz7.48-2  8370  tz7.49  8373  oalim  8456  omlim  8457  oelim  8458  oaordi  8470  oalimcl  8484  oaass  8485  omordi  8490  omlimcl  8502  odi  8503  omass  8504  omeulem1  8506  omeulem2  8507  omopth2  8508  oewordri  8516  oeordsuc  8518  oelimcl  8524  oeeui  8526  oaabs2  8573  omabs  8575  naddssim  8609  naddel12  8624  naddsuc2  8625  omxpenlem  9001  hartogs  9440  card2on  9450  cantnfle  9571  cantnflt  9572  cantnfp1lem3  9580  cantnfp1  9581  oemapvali  9584  cantnflem1b  9586  cantnflem1c  9587  cantnflem1d  9588  cantnflem1  9589  cantnflem2  9590  cantnflem3  9591  cantnflem4  9592  cantnf  9593  cnfcomlem  9599  cnfcom3lem  9603  cnfcom3  9604  r1ordg  9681  r1val3  9741  tskwe  9853  iscard  9878  cardmin2  9902  infxpenlem  9914  infxpenc2lem2  9921  alephordi  9975  alephord2i  9978  alephle  9989  cardaleph  9990  cfub  10150  cfsmolem  10171  zorn2lem5  10401  zorn2lem6  10402  ttukeylem6  10415  ttukeylem7  10416  ondomon  10464  cardmin  10465  alephval2  10473  alephreg  10483  smobeth  10487  winainflem  10594  inar1  10676  inatsk  10679  sltval2  27605  sltres  27611  nosepeq  27634  nosupno  27652  nosupres  27656  nosupbnd1lem1  27657  nosupbnd2lem1  27664  nosupbnd2  27665  noinfno  27667  noinfres  27671  noinfbnd1lem1  27672  noinfbnd2lem1  27679  noinfbnd2  27680  oldlim  27842  oldbday  27856  fineqvnttrclselem2  35153  dfrdg2  35848  dfrdg4  36006  ontopbas  36483  onpsstopbas  36485  onint1  36504  onelord  43358  cantnfresb  43431  oawordex2  43433  oacl2g  43437  omabs2  43439  omcl2  43440  tfsconcatfv2  43447  tfsconcatfv  43448  tfsconcatrn  43449  tfsconcat0i  43452  ofoafg  43461  ofoaass  43467  oaun3lem1  43481  oaun3lem2  43482  oadif1lem  43486  oadif1  43487  nadd2rabtr  43491  nadd1suc  43499  naddgeoa  43501  naddwordnexlem0  43503  naddwordnexlem1  43504  naddwordnexlem3  43506  oawordex3  43507  naddwordnexlem4  43508  omssrncard  43647