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

Theorem onelon 4354
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 4339 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelon 4353 . 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 4328   Oncon0 4329
This theorem is referenced by:  oneli  4437  ssorduni  4514  unon  4559  tfindsg2  4589  dfom2  4595  ordom  4602  onfununi  6291  onnseq  6294  tz7.48-2  6387  tz7.49  6390  oalim  6464  omlim  6465  oelim  6466  oaordi  6477  oalimcl  6491  oaass  6492  omordi  6497  omlimcl  6509  odi  6510  omass  6511  omeulem1  6513  omeulem2  6514  omopth2  6515  oewordri  6523  oeordsuc  6525  oelimcl  6531  oeeui  6533  oaabs2  6576  omabs  6578  omxpenlem  6896  hartogs  7192  card2on  7201  cantnfle  7305  cantnflt  7306  cantnfp1lem2  7314  cantnfp1lem3  7315  cantnfp1  7316  oemapvali  7319  cantnflem1b  7321  cantnflem1c  7322  cantnflem1d  7323  cantnflem1  7324  cantnflem2  7325  cantnflem3  7326  cantnflem4  7327  cantnf  7328  cnfcomlem  7335  cnfcom3lem  7339  cnfcom3  7340  r1ordg  7383  r1val3  7443  tskwe  7516  iscard  7541  cardmin2  7564  infxpenlem  7574  infxpenc2lem2  7580  alephordi  7634  alephord2i  7637  alephle  7648  cardaleph  7649  cfub  7808  cfsmolem  7829  zorn2lem5  8060  zorn2lem6  8061  ttukeylem6  8074  ttukeylem7  8075  ondomon  8118  cardmin  8119  alephval2  8127  alephreg  8137  smobeth  8141  winainflem  8248  inar1  8330  inatsk  8333  dfrdg2  23486  tfrALTlem  23610  sltval2  23643  sltres  23651  axdenselem5  23673  axdenselem7  23675  axfelem6  23685  axfelem18  23697  axfelem19  23698  axfelem20  23699  axfelem22  23701  dfrdg4  23828  ontopbas  24207  onpsstopbas  24209  onint1  24228  vtarsu  25218  tartarmap  25220
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 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152
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 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-tr 4054  df-eprel 4242  df-po 4251  df-so 4252  df-fr 4289  df-we 4291  df-ord 4332  df-on 4333
  Copyright terms: Public domain W3C validator