This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem domsdomtr

Description: Transitivity of dominance and strict dominance. Theorem 22(ii) of Suppes p. 97. (Contributed by NM, 10-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion domsdomtr 
|- ( ( A ~<_ B /\ B ~< C ) -> A ~< C )

Proof

Step Hyp Ref Expression
1 sdomdom 
 |-  ( B ~< C -> B ~<_ C )
2 domtr 
 |-  ( ( A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
3 1 2 sylan2 
 |-  ( ( A ~<_ B /\ B ~< C ) -> A ~<_ C )
4 simpr 
 |-  ( ( A ~<_ B /\ B ~< C ) -> B ~< C )
5 ensym 
 |-  ( A ~~ C -> C ~~ A )
6 simpl 
 |-  ( ( A ~<_ B /\ B ~< C ) -> A ~<_ B )
7 endomtr 
 |-  ( ( C ~~ A /\ A ~<_ B ) -> C ~<_ B )
8 5 6 7 syl2anr 
 |-  ( ( ( A ~<_ B /\ B ~< C ) /\ A ~~ C ) -> C ~<_ B )
9 domnsym 
 |-  ( C ~<_ B -> -. B ~< C )
10 8 9 syl 
 |-  ( ( ( A ~<_ B /\ B ~< C ) /\ A ~~ C ) -> -. B ~< C )
11 10 ex 
 |-  ( ( A ~<_ B /\ B ~< C ) -> ( A ~~ C -> -. B ~< C ) )
12 4 11 mt2d 
 |-  ( ( A ~<_ B /\ B ~< C ) -> -. A ~~ C )
13 brsdom 
 |-  ( A ~< C <-> ( A ~<_ C /\ -. A ~~ C ) )
14 3 12 13 sylanbrc 
 |-  ( ( A ~<_ B /\ B ~< C ) -> A ~< C )