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

Theorem onelon 4593
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 4578 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelon 4592 . 2  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  e.  On )
31, 2sylan 458 1  |-  ( ( A  e.  On  /\  B  e.  A )  ->  B  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   Ord word 4567   Oncon0 4568
This theorem is referenced by:  oneli  4675  ssorduni  4752  unon  4797  tfindsg2  4827  dfom2  4833  ordom  4840  onfununi  6589  onnseq  6592  tz7.48-2  6685  tz7.49  6688  oalim  6762  omlim  6763  oelim  6764  oaordi  6775  oalimcl  6789  oaass  6790  omordi  6795  omlimcl  6807  odi  6808  omass  6809  omeulem1  6811  omeulem2  6812  omopth2  6813  oewordri  6821  oeordsuc  6823  oelimcl  6829  oeeui  6831  oaabs2  6874  omabs  6876  omxpenlem  7195  hartogs  7497  card2on  7506  cantnfle  7610  cantnflt  7611  cantnfp1lem2  7619  cantnfp1lem3  7620  cantnfp1  7621  oemapvali  7624  cantnflem1b  7626  cantnflem1c  7627  cantnflem1d  7628  cantnflem1  7629  cantnflem2  7630  cantnflem3  7631  cantnflem4  7632  cantnf  7633  cnfcomlem  7640  cnfcom3lem  7644  cnfcom3  7645  r1ordg  7688  r1val3  7748  tskwe  7821  iscard  7846  cardmin2  7869  infxpenlem  7879  infxpenc2lem2  7885  alephordi  7939  alephord2i  7942  alephle  7953  cardaleph  7954  cfub  8113  cfsmolem  8134  zorn2lem5  8364  zorn2lem6  8365  ttukeylem6  8378  ttukeylem7  8379  ondomon  8422  cardmin  8423  alephval2  8431  alephreg  8441  smobeth  8445  winainflem  8552  inar1  8634  inatsk  8637  dfrdg2  25402  tfrALTlem  25526  sltval2  25560  sltres  25568  nodenselem5  25589  nodenselem7  25591  nobndlem6  25601  nobndup  25604  dfrdg4  25740  ontopbas  26121  onpsstopbas  26123  onint1  26142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pr 4390
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-opab 4254  df-tr 4290  df-eprel 4481  df-po 4490  df-so 4491  df-fr 4528  df-we 4530  df-ord 4571  df-on 4572
  Copyright terms: Public domain W3C validator