MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  onelon Structured version   Unicode version

Theorem onelon 4744
Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
Assertion
Ref Expression
onelon  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )

Proof of Theorem onelon
StepHypRef Expression
1 eloni 4729 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelon 4743 . 2  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  e.  On )
31, 2sylan 471 1  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   Ord word 4718   Oncon0 4719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-tr 4386  df-eprel 4632  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723
This theorem is referenced by:  oneli  4826  ssorduni  6397  unon  6442  tfindsg2  6472  dfom2  6478  ordom  6485  onfununi  6802  onnseq  6805  tz7.48-2  6897  tz7.49  6900  oalim  6972  omlim  6973  oelim  6974  oaordi  6985  oalimcl  6999  oaass  7000  omordi  7005  omlimcl  7017  odi  7018  omass  7019  omeulem1  7021  omeulem2  7022  omopth2  7023  oewordri  7031  oeordsuc  7033  oelimcl  7039  oeeui  7041  oaabs2  7084  omabs  7086  omxpenlem  7412  hartogs  7758  card2on  7769  cantnfle  7879  cantnflt  7880  cantnfp1lem2  7887  cantnfp1lem3  7888  cantnfp1  7889  oemapvali  7892  cantnflem1b  7894  cantnflem1c  7895  cantnflem1d  7896  cantnflem1  7897  cantnflem2  7898  cantnflem3  7899  cantnflem4  7900  cantnf  7901  cantnfleOLD  7909  cantnfltOLD  7910  cantnfp1lem2OLD  7913  cantnfp1lem3OLD  7914  cantnfp1OLD  7915  cantnflem1bOLD  7917  cantnflem1cOLD  7918  cantnflem1dOLD  7919  cantnflem1OLD  7920  cantnflem3OLD  7921  cantnflem4OLD  7922  cantnfOLD  7923  cnfcomlem  7932  cnfcom3lem  7936  cnfcom3  7937  cnfcomlemOLD  7940  cnfcom3lemOLD  7944  cnfcom3OLD  7945  r1ordg  7985  r1val3  8045  tskwe  8120  iscard  8145  cardmin2  8168  infxpenlem  8180  infxpenc2lem2  8186  infxpenc2lem2OLD  8190  alephordi  8244  alephord2i  8247  alephle  8258  cardaleph  8259  cfub  8418  cfsmolem  8439  zorn2lem5  8669  zorn2lem6  8670  ttukeylem6  8683  ttukeylem7  8684  ondomon  8727  cardmin  8728  alephval2  8736  alephreg  8746  smobeth  8750  winainflem  8860  inar1  8942  inatsk  8945  dfrdg2  27609  sltval2  27797  sltres  27805  nodenselem5  27826  nodenselem7  27828  nobndlem6  27838  nobndup  27841  dfrdg4  27981  ontopbas  28274  onpsstopbas  28276  onint1  28295
  Copyright terms: Public domain W3C validator