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

Theorem sdomdomtr 9039
Description: Transitivity of strict dominance and dominance. Theorem 22(iii) of [Suppes] p. 97. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
sdomdomtr ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)

Proof of Theorem sdomdomtr
StepHypRef Expression
1 sdomdom 8918 . . 3 (𝐴𝐵𝐴𝐵)
2 domtr 8945 . . 3 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
31, 2sylan 581 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
4 simpl 482 . . 3 ((𝐴𝐵𝐵𝐶) → 𝐴𝐵)
5 simpr 484 . . . . . 6 ((𝐴𝐵𝐵𝐶) → 𝐵𝐶)
6 ensym 8941 . . . . . 6 (𝐴𝐶𝐶𝐴)
7 domentr 8951 . . . . . 6 ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)
85, 6, 7syl2an 597 . . . . 5 (((𝐴𝐵𝐵𝐶) ∧ 𝐴𝐶) → 𝐵𝐴)
9 domnsym 9032 . . . . 5 (𝐵𝐴 → ¬ 𝐴𝐵)
108, 9syl 17 . . . 4 (((𝐴𝐵𝐵𝐶) ∧ 𝐴𝐶) → ¬ 𝐴𝐵)
1110ex 412 . . 3 ((𝐴𝐵𝐵𝐶) → (𝐴𝐶 → ¬ 𝐴𝐵))
124, 11mt2d 136 . 2 ((𝐴𝐵𝐵𝐶) → ¬ 𝐴𝐶)
13 brsdom 8912 . 2 (𝐴𝐶 ↔ (𝐴𝐶 ∧ ¬ 𝐴𝐶))
143, 12, 13sylanbrc 584 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   class class class wbr 5086  cen 8881  cdom 8882  csdm 8883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pow 5300  ax-pr 5368  ax-un 7680
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887
This theorem is referenced by:  sdomentr  9040  fodomfibOLD  9232  marypha1lem  9337  r1sdom  9687  infxpenlem  9924  infunsdom1  10123  fin56  10304  fodomb  10437  pwcfsdom  10495  cfpwsdom  10496  canthp1lem2  10565  gchpwdom  10582  gchhar  10591  gchina  10611  tsksdom  10668  tskpr  10682  tskcard  10693  gruina  10730  domalom  37716  lindsenlbs  37927
  Copyright terms: Public domain W3C validator