Theorem onelon 6343

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Ord word 6317  Oncon0 6318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6321  df-on 6322

This theorem is referenced by:  oneli  6433  ssorduni  7726  unon  7775  tfindsg2  7806  dfom2  7812  trom  7819  onfununi  8275  onnseq  8278  dfrecs3  8306  tz7.48-2  8375  tz7.49  8378  oalim  8461  omlim  8462  oelim  8463  oaordi  8475  oalimcl  8489  oaass  8490  omordi  8495  omlimcl  8507  odi  8508  omass  8509  omeulem1  8511  omeulem2  8512  omopth2  8513  oewordri  8522  oeordsuc  8524  oelimcl  8530  oeeui  8532  oaabs2  8579  omabs  8581  naddssim  8615  naddel12  8630  naddsuc2  8631  omxpenlem  9010  hartogs  9453  card2on  9463  cantnfle  9584  cantnflt  9585  cantnfp1lem3  9593  cantnfp1  9594  oemapvali  9597  cantnflem1b  9599  cantnflem1c  9600  cantnflem1d  9601  cantnflem1  9602  cantnflem2  9603  cantnflem3  9604  cantnflem4  9605  cantnf  9606  cnfcomlem  9612  cnfcom3lem  9616  cnfcom3  9617  r1ordg  9694  r1val3  9754  tskwe  9866  iscard  9891  cardmin2  9915  infxpenlem  9927  infxpenc2lem2  9934  alephordi  9988  alephord2i  9991  alephle  10002  cardaleph  10003  cfub  10163  cfsmolem  10184  zorn2lem5  10414  zorn2lem6  10415  ttukeylem6  10428  ttukeylem7  10429  ondomon  10477  cardmin  10478  alephval2  10487  alephreg  10497  smobeth  10501  winainflem  10608  inar1  10690  inatsk  10693  sltval2  27628  sltres  27634  nosepeq  27657  nosupno  27675  nosupres  27679  nosupbnd1lem1  27680  nosupbnd2lem1  27687  nosupbnd2  27688  noinfno  27690  noinfres  27694  noinfbnd1lem1  27695  noinfbnd2lem1  27702  noinfbnd2  27703  oldlim  27869  oldbday  27883  fineqvnttrclselem2  35259  dfrdg2  35968  dfrdg4  36126  ontopbas  36603  onpsstopbas  36605  onint1  36624  onelord  43529  cantnfresb  43602  oawordex2  43604  oacl2g  43608  omabs2  43610  omcl2  43611  tfsconcatfv2  43618  tfsconcatfv  43619  tfsconcatrn  43620  tfsconcat0i  43623  ofoafg  43632  ofoaass  43638  oaun3lem1  43652  oaun3lem2  43653  oadif1lem  43657  oadif1  43658  nadd2rabtr  43662  nadd1suc  43670  naddgeoa  43672  naddwordnexlem0  43674  naddwordnexlem1  43675  naddwordnexlem3  43677  oawordex3  43678  naddwordnexlem4  43679  omssrncard  43817