Theorem sdomdomtr

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)

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

Proof

Step	Hyp	Ref	Expression
1		sdomdom	|- ( A ~< B -> A ~<_ B )
2		domtr	|- ( ( A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
3	1 2	sylan	|- ( ( A ~< B /\ B ~<_ C ) -> A ~<_ C )
4		simpl	|- ( ( A ~< B /\ B ~<_ C ) -> A ~< B )
5		simpr	|- ( ( A ~< B /\ B ~<_ C ) -> B ~<_ C )
6		ensym	|- ( A ~~ C -> C ~~ A )
7		domentr	|- ( ( B ~<_ C /\ C ~~ A ) -> B ~<_ A )
8	5 6 7	syl2an	|- ( ( ( A ~< B /\ B ~<_ C ) /\ A ~~ C ) -> B ~<_ A )
9		domnsym	|- ( B ~<_ A -> -. A ~< B )
10	8 9	syl	|- ( ( ( A ~< B /\ B ~<_ C ) /\ A ~~ C ) -> -. A ~< B )
11	10	ex	|- ( ( A ~< B /\ B ~<_ C ) -> ( A ~~ C -> -. A ~< B ) )
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 )