Theorem onelon 6401

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099  Ord word 6375  Oncon0 6376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-tr 5271  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-ord 6379  df-on 6380

This theorem is referenced by:  oneli  6490  ssorduni  7787  unon  7840  tfindsg2  7872  dfom2  7878  trom  7885  onfununi  8371  onnseq  8374  dfrecs3  8402  dfrecs3OLD  8403  tz7.48-2  8472  tz7.49  8475  oalim  8562  omlim  8563  oelim  8564  oaordi  8576  oalimcl  8590  oaass  8591  omordi  8596  omlimcl  8608  odi  8609  omass  8610  omeulem1  8612  omeulem2  8613  omopth2  8614  oewordri  8622  oeordsuc  8624  oelimcl  8630  oeeui  8632  oaabs2  8679  omabs  8681  naddssim  8715  naddel12  8730  omxpenlem  9111  hartogs  9587  card2on  9597  cantnfle  9714  cantnflt  9715  cantnfp1lem3  9723  cantnfp1  9724  oemapvali  9727  cantnflem1b  9729  cantnflem1c  9730  cantnflem1d  9731  cantnflem1  9732  cantnflem2  9733  cantnflem3  9734  cantnflem4  9735  cantnf  9736  cnfcomlem  9742  cnfcom3lem  9746  cnfcom3  9747  r1ordg  9821  r1val3  9881  tskwe  9993  iscard  10018  cardmin2  10042  infxpenlem  10056  infxpenc2lem2  10063  alephordi  10117  alephord2i  10120  alephle  10131  cardaleph  10132  cfub  10292  cfsmolem  10313  zorn2lem5  10543  zorn2lem6  10544  ttukeylem6  10557  ttukeylem7  10558  ondomon  10606  cardmin  10607  alephval2  10615  alephreg  10625  smobeth  10629  winainflem  10736  inar1  10818  inatsk  10821  sltval2  27686  sltres  27692  nosepeq  27715  nosupno  27733  nosupres  27737  nosupbnd1lem1  27738  nosupbnd2lem1  27745  nosupbnd2  27746  noinfno  27748  noinfres  27752  noinfbnd1lem1  27753  noinfbnd2lem1  27760  noinfbnd2  27761  oldlim  27910  oldbday  27924  dfrdg2  35619  dfrdg4  35775  ontopbas  36140  onpsstopbas  36142  onint1  36161  onelord  42916  cantnfresb  42990  oawordex2  42992  oacl2g  42996  omabs2  42998  omcl2  42999  tfsconcatfv2  43006  tfsconcatfv  43007  tfsconcatrn  43008  tfsconcat0i  43011  ofoafg  43020  ofoaass  43026  oaun3lem1  43040  oaun3lem2  43041  oadif1lem  43045  oadif1  43046  nadd2rabtr  43050  nadd1suc  43058  naddsuc2  43059  naddgeoa  43061  naddwordnexlem0  43063  naddwordnexlem1  43064  naddwordnexlem3  43066  oawordex3  43067  naddwordnexlem4  43068  omssrncard  43207