Theorem domnsym

Description: Theorem 22(i) of Suppes p. 97. (Contributed by NM, 10-Jun-1998)

	Ref	Expression
Assertion	domnsym	⊢ ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		brdom2	⊢ ( 𝐴 ≼ 𝐵 ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) )
2		sdomnsym	⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴 )
3		sdomnen	⊢ ( 𝐵 ≺ 𝐴 → ¬ 𝐵 ≈ 𝐴 )
4		ensym	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
5	3 4	nsyl3	⊢ ( 𝐴 ≈ 𝐵 → ¬ 𝐵 ≺ 𝐴 )
6	2 5	jaoi	⊢ ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )
7	1 6	sylbi	⊢ ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴 )