Theorem domnsym

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

	Ref	Expression
Assertion	domnsym	$$⊢A\preccurlyeq B\to \neg B\prec A$$

Proof

Step	Hyp	Ref	Expression
1		brdom2	$$⊢A\preccurlyeq B\leftrightarrow \left(A\prec B\vee A\approx B\right)$$
2		sdomnsym	$$⊢A\prec B\to \neg B\prec A$$
3		sdomnen	$$⊢B\prec A\to \neg B\approx A$$
4		ensym	$$⊢A\approx B\to B\approx A$$
5	3 4	nsyl3	$$⊢A\approx B\to \neg B\prec A$$
6	2 5	jaoi	$$⊢\left(A\prec B\vee A\approx B\right)\to \neg B\prec A$$
7	1 6	sylbi	$$⊢A\preccurlyeq B\to \neg B\prec A$$