Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		sdomdom	$⊢ A ≺ B \to A ≼ B$
2		domtr	$⊢ (A ≼ B \land B ≼ C) \to A ≼ C$
3	1 2	sylan	$⊢ (A ≺ B \land B ≼ C) \to A ≼ C$
4		simpl	$⊢ (A ≺ B \land B ≼ C) \to A ≺ B$
5		simpr	$⊢ (A ≺ B \land B ≼ C) \to B ≼ C$
6		ensym	$⊢ A \approx C \to C \approx A$
7		domentr	$⊢ (B ≼ C \land C \approx A) \to B ≼ A$
8	5 6 7	syl2an	$⊢ ((A ≺ B \land B ≼ C) \land A \approx C) \to B ≼ A$
9		domnsym	$⊢ B ≼ A \to \neg A ≺ B$
10	8 9	syl	$⊢ ((A ≺ B \land B ≼ C) \land A \approx C) \to \neg A ≺ B$
11	10	ex	$⊢ (A ≺ B \land B ≼ C) \to (A \approx C \to \neg A ≺ B)$
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$