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	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≺ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		sdomdom	⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
2		domtr	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
3	1 2	sylan	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
4		simpl	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≺ 𝐵 )
5		simpr	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐵 ≼ 𝐶 )
6		ensym	⊢ ( 𝐴 ≈ 𝐶 → 𝐶 ≈ 𝐴 )
7		domentr	⊢ ( ( 𝐵 ≼ 𝐶 ∧ 𝐶 ≈ 𝐴 ) → 𝐵 ≼ 𝐴 )
8	5 6 7	syl2an	⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) ∧ 𝐴 ≈ 𝐶 ) → 𝐵 ≼ 𝐴 )
9		domnsym	⊢ ( 𝐵 ≼ 𝐴 → ¬ 𝐴 ≺ 𝐵 )
10	8 9	syl	⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) ∧ 𝐴 ≈ 𝐶 ) → ¬ 𝐴 ≺ 𝐵 )
11	10	ex	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ≈ 𝐶 → ¬ 𝐴 ≺ 𝐵 ) )
12	4 11	mt2d	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ¬ 𝐴 ≈ 𝐶 )
13		brsdom	⊢ ( 𝐴 ≺ 𝐶 ↔ ( 𝐴 ≼ 𝐶 ∧ ¬ 𝐴 ≈ 𝐶 ) )
14	3 12 13	sylanbrc	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≺ 𝐶 )