This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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