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 ∧ 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