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

Metamath Proof Explorer

Theorem sdomnsym

Description: Strict dominance is asymmetric. Theorem 21(ii) of Suppes p. 97. (Contributed by NM, 8-Jun-1998)

Ref Expression
Assertion sdomnsym ( 𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴 )

Proof

Step Hyp Ref Expression
1 sdomnen ⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )
2 sdomdom ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
3 sdomdom ⊢ ( 𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴 )
4 sbth ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 )
5 2 3 4 syl2an ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐴 ) → 𝐴 ≈ 𝐵 )
6 1 5 mtand ⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴 )