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

Theorem domnsym 6989
Description: Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.)
Assertion
Ref Expression
domnsym  |-  ( A  ~<_  B  ->  -.  B  ~<  A )

Proof of Theorem domnsym
StepHypRef Expression
1 brdom2 6893 . 2  |-  ( A  ~<_  B  <->  ( A  ~<  B  \/  A  ~~  B
) )
2 sdomnsym 6988 . . 3  |-  ( A 
~<  B  ->  -.  B  ~<  A )
3 sdomnen 6892 . . . 4  |-  ( B 
~<  A  ->  -.  B  ~~  A )
4 ensym 6912 . . . 4  |-  ( A 
~~  B  ->  B  ~~  A )
53, 4nsyl3 111 . . 3  |-  ( A 
~~  B  ->  -.  B  ~<  A )
62, 5jaoi 368 . 2  |-  ( ( A  ~<  B  \/  A  ~~  B )  ->  -.  B  ~<  A )
71, 6sylbi 187 1  |-  ( A  ~<_  B  ->  -.  B  ~<  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357   class class class wbr 4025    ~~ cen 6862    ~<_ cdom 6863    ~< csdm 6864
This theorem is referenced by:  sdom0  6995  sdomdomtr  6996  domsdomtr  6998  sdomdif  7011  onsdominel  7012  nndomo  7056  sdom1  7064  fofinf1o  7139  carddom2  7612  fidomtri  7628  fidomtri2  7629  infxpenlem  7643  alephordi  7703  infdif  7837  infdif2  7838  cfslbn  7895  cfslb2n  7896  fincssdom  7951  fin45  8020  domtriom  8071  alephval2  8196  alephreg  8206  pwcfsdom  8207  cfpwsdom  8208  pwfseqlem3  8284  gchhar  8295  gchpwdom  8298  gchaleph  8299  hargch  8301  winainflem  8317  rankcf  8401  tskcard  8405  vdwlem12  13041  odinf  14878  rectbntr0  18339  erdszelem10  23733  finminlem  26242  fphpd  26910
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-er 6662  df-en 6866  df-dom 6867  df-sdom 6868
  Copyright terms: Public domain W3C validator