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

Theorem onelon 5467
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 5452 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelon 5466 . 2  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  e.  On )
31, 2sylan 473 1  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1870   Ord word 5441   Oncon0 5442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-tr 4521  df-eprel 4765  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-ord 5445  df-on 5446
This theorem is referenced by:  oneli  5549  ssorduni  6626  unon  6672  tfindsg2  6702  dfom2  6708  ordom  6715  onfununi  7068  onnseq  7071  dfrecs3  7099  tz7.48-2  7167  tz7.49  7170  oalim  7242  omlim  7243  oelim  7244  oaordi  7255  oalimcl  7269  oaass  7270  omordi  7275  omlimcl  7287  odi  7288  omass  7289  omeulem1  7291  omeulem2  7292  omopth2  7293  oewordri  7301  oeordsuc  7303  oelimcl  7309  oeeui  7311  oaabs2  7354  omabs  7356  omxpenlem  7679  hartogs  8059  card2on  8069  cantnfle  8175  cantnflt  8176  cantnfp1lem2  8183  cantnfp1lem3  8184  cantnfp1  8185  oemapvali  8188  cantnflem1b  8190  cantnflem1c  8191  cantnflem1d  8192  cantnflem1  8193  cantnflem2  8194  cantnflem3  8195  cantnflem4  8196  cantnf  8197  cnfcomlem  8203  cnfcom3lem  8207  cnfcom3  8208  r1ordg  8248  r1val3  8308  tskwe  8383  iscard  8408  cardmin2  8431  infxpenlem  8443  infxpenc2lem2  8449  alephordi  8503  alephord2i  8506  alephle  8517  cardaleph  8518  cfub  8677  cfsmolem  8698  zorn2lem5  8928  zorn2lem6  8929  ttukeylem6  8942  ttukeylem7  8943  ondomon  8986  cardmin  8987  alephval2  8995  alephreg  9005  smobeth  9009  winainflem  9117  inar1  9199  inatsk  9202  dfrdg2  30229  sltval2  30330  sltres  30338  nodenselem5  30359  nodenselem7  30361  nobndlem6  30371  nobndup  30374  dfrdg4  30503  ontopbas  30873  onpsstopbas  30875  onint1  30894
  Copyright terms: Public domain W3C validator