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

Theorem sdomdom 7138
Description: Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.)
Assertion
Ref Expression
sdomdom  |-  ( A 
~<  B  ->  A  ~<_  B )

Proof of Theorem sdomdom
StepHypRef Expression
1 brsdom 7133 . 2  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
21simplbi 448 1  |-  ( A 
~<  B  ->  A  ~<_  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   class class class wbr 4215    ~~ cen 7109    ~<_ cdom 7110    ~< csdm 7111
This theorem is referenced by:  domdifsn  7194  sdomnsym  7235  sdomdomtr  7243  domsdomtr  7245  sdomtr  7248  sucdom2  7306  sucxpdom  7321  isfinite2  7368  pwfi  7405  card2on  7525  fidomtri2  7886  prdom2  7895  infxpenlem  7900  indcardi  7927  alephnbtwn2  7958  alephsucdom  7965  alephdom  7967  dfac13  8027  cdalepw  8081  infcdaabs  8091  infdif  8094  infunsdom1  8098  infunsdom  8099  infxp  8100  cfslb2n  8153  sdom2en01  8187  isfin32i  8250  fin34  8275  fin67  8280  hsmexlem1  8311  hsmex3  8319  entri3  8439  unirnfdomd  8447  alephexp1  8459  cfpwsdom  8464  gchdomtri  8509  canthp1  8534  pwfseqlem5  8543  gchcdaidm  8548  gchxpidm  8549  gchpwdom  8550  hargch  8553  gchaclem  8558  gchhar  8559  gchac  8561  inawinalem  8569  inar1  8655  rankcf  8657  tskuni  8663  grothac  8710  rpnnen  12831  rexpen  12832  aleph1irr  12850  dis1stc  17567  hauspwdom  17569  ovolfi  19395  sigaclfu  24507  sibfof  24659  heiborlem3  26536  harinf  27119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-br 4216  df-sdom 7115
  Copyright terms: Public domain W3C validator