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 ∧ B ≺ C → A ≺ C

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ B ≺ C → B ≼ C
2 domtr ⊢ A ≼ B ∧ B ≼ C → A ≼ C
3 1 2 sylan2 ⊢ A ≼ B ∧ B ≺ C → A ≼ C
4 simpr ⊢ A ≼ B ∧ B ≺ C → B ≺ C
5 ensym ⊢ A ≈ C → C ≈ A
6 simpl ⊢ A ≼ B ∧ B ≺ C → A ≼ B
7 endomtr ⊢ C ≈ A ∧ A ≼ B → C ≼ B
8 5 6 7 syl2anr ⊢ A ≼ B ∧ B ≺ C ∧ A ≈ C → C ≼ B
9 domnsym ⊢ C ≼ B → ¬ B ≺ C
10 8 9 syl ⊢ A ≼ B ∧ B ≺ C ∧ A ≈ C → ¬ B ≺ C
11 10 ex ⊢ A ≼ B ∧ B ≺ C → A ≈ C → ¬ B ≺ C
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