Theorem onelon 6376

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Ord word 6350  Oncon0 6351

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248  ax-pr 5390

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6354  df-on 6355

This theorem is used by:  oneli  6467  ssorduni  7776  unon  7825  tfindsg2  7856  dfom2  7862  trom  7869  onfununi  8327  onnseq  8330  dfrecs3  8358  tz7.48-2  8430  tz7.49  8433  oalim  8518  omlim  8519  oelim  8520  oaordi  8532  oalimcl  8546  oaass  8547  omordi  8552  omlimcl  8564  odi  8565  omass  8566  omeulem1  8568  omeulem2  8569  omopth2  8570  oewordri  8579  oeordsuc  8581  oelimcl  8587  oeeui  8589  oaabs2  8636  omabs  8638  naddssim  8673  naddel12  8688  naddsuc2  8689  omxpenlem  9075  hartogs  9516  card2on  9526  cantnfle  9650  cantnflt  9651  cantnfp1lem3  9659  cantnfp1  9660  oemapvali  9663  cantnflem1b  9665  cantnflem1c  9666  cantnflem1d  9667  cantnflem1  9668  cantnflem2  9669  cantnflem3  9670  cantnflem4  9671  cantnf  9672  cnfcomlem  9678  cnfcom3lem  9682  cnfcom3  9683  r1ordg  9760  r1val3  9823  tskwe  10003  iscard  10028  cardmin2  10052  infxpenlem  10064  infxpenc2lem2  10071  alephordi  10125  alephord2i  10128  alephle  10139  cardaleph  10140  cfub  10298  cfsmolem  10320  zorn2lem5  10550  zorn2lem6  10551  ttukeylem6  10564  ttukeylem7  10565  ondomon  10619  cardmin  10620  alephval2  10629  alephreg  10639  smobeth  10643  winainflem  10750  inar1  10832  inatsk  10835  ltsval2  27947  ltsres  27953  nosepeq  27976  nosupno  27994  nosupres  27998  nosupbnd1lem1  27999  nosupbnd2lem1  28006  nosupbnd2  28007  noinfno  28009  noinfres  28013  noinfbnd1lem1  28014  noinfbnd2lem1  28021  noinfbnd2  28022  oldlim  28207  oldbday  28221  fineqvnttrclselem2  35715  dfrdg2  36479  dfrdg4  36637  nmulcom  36865  onelond  36870  nmuladdss  36884  nmulel1  36886  ltnmul  36887  nmulle  36888  ontopbas  37138  onpsstopbas  37140  onint1  37159  onelord  44196  cantnfresb  44269  oawordex2  44271  oacl2g  44275  omabs2  44277  omcl2  44278  tfsconcatfv2  44285  tfsconcatfv  44286  tfsconcatrn  44287  tfsconcat0i  44290  ofoafg  44299  ofoaass  44305  oaun3lem1  44319  oaun3lem2  44320  oadif1lem  44324  oadif1  44325  nadd2rabtr  44329  nadd1suc  44337  naddgeoa  44339  naddwordnexlem0  44341  naddwordnexlem1  44342  naddwordnexlem3  44344  oawordex3  44345  naddwordnexlem4  44346  omssrncard  44484