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 )