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 \land B ≺ C) \to A ≺ C$

Proof

Step	Hyp	Ref	Expression
1		sdomdom	$⊢ B ≺ C \to B ≼ C$
2		domtr	$⊢ (A ≼ B \land B ≼ C) \to A ≼ C$
3	1 2	sylan2	$⊢ (A ≼ B \land B ≺ C) \to A ≼ C$
4		simpr	$⊢ (A ≼ B \land B ≺ C) \to B ≺ C$
5		ensym	$⊢ A \approx C \to C \approx A$
6		simpl	$⊢ (A ≼ B \land B ≺ C) \to A ≼ B$
7		endomtr	$⊢ (C \approx A \land A ≼ B) \to C ≼ B$
8	5 6 7	syl2anr	$⊢ ((A ≼ B \land B ≺ C) \land A \approx C) \to C ≼ B$
9		domnsym	$⊢ C ≼ B \to \neg B ≺ C$
10	8 9	syl	$⊢ ((A ≼ B \land B ≺ C) \land A \approx C) \to \neg B ≺ C$
11	10	ex	$⊢ (A ≼ B \land B ≺ C) \to (A \approx C \to \neg B ≺ C)$
12	4 11	mt2d	$⊢ (A ≼ B \land B ≺ C) \to \neg A \approx C$
13		brsdom	$⊢ A ≺ C \leftrightarrow (A ≼ C \land \neg A \approx C)$
14	3 12 13	sylanbrc	$⊢ (A ≼ B \land B ≺ C) \to A ≺ C$