Theorem onelon 6405

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  Ord word 6379  Oncon0 6380

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-tr 5216  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6383  df-on 6384

This theorem is used by:  oneli  6496  ssorduni  7817  unon  7866  tfindsg2  7897  dfom2  7903  trom  7910  onfununi  8377  onnseq  8380  dfrecs3  8408  tz7.48-2  8480  tz7.49  8483  oalim  8568  omlim  8569  oelim  8570  oaordi  8582  oalimcl  8596  oaass  8597  omordi  8602  omlimcl  8614  odi  8615  omass  8616  omeulem1  8618  omeulem2  8619  omopth2  8620  oewordri  8629  oeordsuc  8631  oelimcl  8637  oeeui  8639  oaabs2  8686  omabs  8688  naddssim  8723  naddel12  8738  naddsuc2  8739  omxpenlem  9125  hartogs  9565  card2on  9575  cantnfle  9699  cantnflt  9700  cantnfp1lem3  9708  cantnfp1  9709  oemapvali  9712  cantnflem1b  9714  cantnflem1c  9715  cantnflem1d  9716  cantnflem1  9717  cantnflem2  9718  cantnflem3  9719  cantnflem4  9720  cantnf  9721  cnfcomlem  9727  cnfcom3lem  9731  cnfcom3  9732  r1ordg  9812  r1val3  9877  tskwe  10058  iscard  10083  cardmin2  10107  infxpenlem  10119  infxpenc2lem2  10126  alephordi  10180  alephord2i  10183  alephle  10194  cardaleph  10195  cfub  10353  cfsmolem  10375  zorn2lem5  10605  zorn2lem6  10606  ttukeylem6  10619  ttukeylem7  10620  ondomon  10674  cardmin  10675  alephval2  10684  alephreg  10694  smobeth  10698  winainflem  10805  inar1  10887  inatsk  10890  ltsval2  28043  ltsres  28049  nosepeq  28072  nosupno  28090  nosupres  28094  nosupbnd1lem1  28095  nosupbnd2lem1  28102  nosupbnd2  28103  noinfno  28105  noinfres  28109  noinfbnd1lem1  28110  noinfbnd2lem1  28117  noinfbnd2  28118  oldlim  28303  oldbday  28317  omeueq  35796  fineqvnttrclselem2  35890  jf1  36010  j0le  36019  k3n0j0lt  36020  dfrdg2  36735  dfrdg4  36893  nmulcom  37121  onelond  37126  nmuladdss  37140  nmulel1  37142  ltnmul  37143  nmulle  37144  ontopbas  37394  onpsstopbas  37396  onint1  37415  onelord  44445  cantnfresb  44518  oawordex2  44520  oacl2g  44524  omabs2  44526  omcl2  44527  tfsconcatfv2  44534  tfsconcatfv  44535  tfsconcatrn  44536  tfsconcat0i  44539  ofoafg  44548  ofoaass  44554  oaun3lem1  44568  oaun3lem2  44569  oadif1lem  44573  oadif1  44574  nadd2rabtr  44578  nadd1suc  44586  naddgeoa  44588  naddwordnexlem0  44590  naddwordnexlem1  44591  naddwordnexlem3  44593  oawordex3  44594  naddwordnexlem4  44595  omssrncard  44733