Theorem onelon 6336

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Ord word 6310  Oncon0 6311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  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 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315

This theorem is referenced by:  oneli  6426  ssorduni  7719  unon  7770  tfindsg2  7802  dfom2  7808  trom  7815  onfununi  8271  onnseq  8274  dfrecs3  8302  tz7.48-2  8371  tz7.49  8374  oalim  8457  omlim  8458  oelim  8459  oaordi  8471  oalimcl  8485  oaass  8486  omordi  8491  omlimcl  8503  odi  8504  omass  8505  omeulem1  8507  omeulem2  8508  omopth2  8509  oewordri  8517  oeordsuc  8519  oelimcl  8525  oeeui  8527  oaabs2  8574  omabs  8576  naddssim  8610  naddel12  8625  naddsuc2  8626  omxpenlem  9002  hartogs  9455  card2on  9465  cantnfle  9586  cantnflt  9587  cantnfp1lem3  9595  cantnfp1  9596  oemapvali  9599  cantnflem1b  9601  cantnflem1c  9602  cantnflem1d  9603  cantnflem1  9604  cantnflem2  9605  cantnflem3  9606  cantnflem4  9607  cantnf  9608  cnfcomlem  9614  cnfcom3lem  9618  cnfcom3  9619  r1ordg  9693  r1val3  9753  tskwe  9865  iscard  9890  cardmin2  9914  infxpenlem  9926  infxpenc2lem2  9933  alephordi  9987  alephord2i  9990  alephle  10001  cardaleph  10002  cfub  10162  cfsmolem  10183  zorn2lem5  10413  zorn2lem6  10414  ttukeylem6  10427  ttukeylem7  10428  ondomon  10476  cardmin  10477  alephval2  10485  alephreg  10495  smobeth  10499  winainflem  10606  inar1  10688  inatsk  10691  sltval2  27584  sltres  27590  nosepeq  27613  nosupno  27631  nosupres  27635  nosupbnd1lem1  27636  nosupbnd2lem1  27643  nosupbnd2  27644  noinfno  27646  noinfres  27650  noinfbnd1lem1  27651  noinfbnd2lem1  27658  noinfbnd2  27659  oldlim  27819  oldbday  27833  dfrdg2  35768  dfrdg4  35924  ontopbas  36401  onpsstopbas  36403  onint1  36422  onelord  43224  cantnfresb  43297  oawordex2  43299  oacl2g  43303  omabs2  43305  omcl2  43306  tfsconcatfv2  43313  tfsconcatfv  43314  tfsconcatrn  43315  tfsconcat0i  43318  ofoafg  43327  ofoaass  43333  oaun3lem1  43347  oaun3lem2  43348  oadif1lem  43352  oadif1  43353  nadd2rabtr  43357  nadd1suc  43365  naddgeoa  43367  naddwordnexlem0  43369  naddwordnexlem1  43370  naddwordnexlem3  43372  oawordex3  43373  naddwordnexlem4  43374  omssrncard  43513