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

Proof

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