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

Theorem onelon 4310
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 4295 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelon 4309 . 2  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  e.  On )
31, 2sylan 459 1  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   Ord word 4284   Oncon0 4285
This theorem is referenced by:  oneli  4391  ssorduni  4468  unon  4513  tfindsg2  4543  dfom2  4549  ordom  4556  onfununi  6244  onnseq  6247  tz7.48-2  6340  tz7.49  6343  oalim  6417  omlim  6418  oelim  6419  oaordi  6430  oalimcl  6444  oaass  6445  omordi  6450  omlimcl  6462  odi  6463  omass  6464  omeulem1  6466  omeulem2  6467  omopth2  6468  oewordri  6476  oeordsuc  6478  oelimcl  6484  oeeui  6486  oaabs2  6529  omabs  6531  omxpenlem  6848  hartogs  7143  card2on  7152  cantnfle  7256  cantnflt  7257  cantnfp1lem2  7265  cantnfp1lem3  7266  cantnfp1  7267  oemapvali  7270  cantnflem1b  7272  cantnflem1c  7273  cantnflem1d  7274  cantnflem1  7275  cantnflem2  7276  cantnflem3  7277  cantnflem4  7278  cantnf  7279  cnfcomlem  7286  cnfcom3lem  7290  cnfcom3  7291  r1ordg  7334  r1val3  7394  tskwe  7467  iscard  7492  cardmin2  7515  infxpenlem  7525  infxpenc2lem2  7531  alephordi  7585  alephord2i  7588  alephle  7599  cardaleph  7600  cfub  7759  cfsmolem  7780  zorn2lem5  8011  zorn2lem6  8012  ttukeylem6  8025  ttukeylem7  8026  ondomon  8067  cardmin  8068  alephval2  8074  alephreg  8084  smobeth  8088  winainflem  8195  inar1  8277  inatsk  8280  dfrdg2  23320  tfrALTlem  23444  sltval2  23477  sltres  23485  axdenselem5  23507  axdenselem7  23509  axfelem6  23519  axfelem18  23531  axfelem19  23532  axfelem20  23533  axfelem22  23535  dfrdg4  23662  ontopbas  24041  onpsstopbas  24043  onint1  24062  vtarsu  25052  tartarmap  25054
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-tr 4011  df-eprel 4198  df-po 4207  df-so 4208  df-fr 4245  df-we 4247  df-ord 4288  df-on 4289
  Copyright terms: Public domain W3C validator