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

Theorem domnsym 8439
Description: Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.)
Assertion
Ref Expression
domnsym (𝐴𝐵 → ¬ 𝐵𝐴)

Proof of Theorem domnsym
StepHypRef Expression
1 brdom2 8336 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 sdomnsym 8438 . . 3 (𝐴𝐵 → ¬ 𝐵𝐴)
3 sdomnen 8335 . . . 4 (𝐵𝐴 → ¬ 𝐵𝐴)
4 ensym 8355 . . . 4 (𝐴𝐵𝐵𝐴)
53, 4nsyl3 136 . . 3 (𝐴𝐵 → ¬ 𝐵𝐴)
62, 5jaoi 843 . 2 ((𝐴𝐵𝐴𝐵) → ¬ 𝐵𝐴)
71, 6sylbi 209 1 (𝐴𝐵 → ¬ 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 833   class class class wbr 4929  cen 8303  cdom 8304  csdm 8305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309
This theorem is referenced by:  sdom0  8445  sdomdomtr  8446  domsdomtr  8448  sdomdif  8461  onsdominel  8462  nndomo  8507  sdom1  8513  fofinf1o  8594  carddom2  9200  fidomtri  9216  fidomtri2  9217  infxpenlem  9233  alephordi  9294  infdif  9429  infdif2  9430  cfslbn  9487  cfslb2n  9488  fincssdom  9543  fin45  9612  domtriom  9663  alephval2  9792  alephreg  9802  pwcfsdom  9803  cfpwsdom  9804  pwfseqlem3  9880  gchpwdom  9890  gchaleph  9891  hargch  9893  gchhar  9899  winainflem  9913  rankcf  9997  tskcard  10001  vdwlem12  16184  odinf  18451  rectbntr0  23143  erdszelem10  32038  finminlem  33193  fphpd  38815
  Copyright terms: Public domain W3C validator