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

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

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
2 domtr ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
3 1 2 sylan ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
4 simpl ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≺ 𝐵 )
5 simpr ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐵 ≼ 𝐶 )
6 ensym ⊢ ( 𝐴 ≈ 𝐶 → 𝐶 ≈ 𝐴 )
7 domentr ⊢ ( ( 𝐵 ≼ 𝐶 ∧ 𝐶 ≈ 𝐴 ) → 𝐵 ≼ 𝐴 )
8 5 6 7 syl2an ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) ∧ 𝐴 ≈ 𝐶 ) → 𝐵 ≼ 𝐴 )
9 domnsym ⊢ ( 𝐵 ≼ 𝐴 → ¬ 𝐴 ≺ 𝐵 )
10 8 9 syl ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) ∧ 𝐴 ≈ 𝐶 ) → ¬ 𝐴 ≺ 𝐵 )
11 10 ex ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ≈ 𝐶 → ¬ 𝐴 ≺ 𝐵 ) )
12 4 11 mt2d ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ¬ 𝐴 ≈ 𝐶 )
13 brsdom ⊢ ( 𝐴 ≺ 𝐶 ↔ ( 𝐴 ≼ 𝐶 ∧ ¬ 𝐴 ≈ 𝐶 ) )
14 3 12 13 sylanbrc ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≺ 𝐶 )