Theorem dfsdom2

Description: Alternate definition of strict dominance. Compare Definition 3 of Suppes p. 97. (Contributed by NM, 31-Mar-1998)

	Ref	Expression
Assertion	dfsdom2	$$⊢\prec =\preccurlyeq \setminus {\preccurlyeq }^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		df-sdom	$$⊢\prec =\preccurlyeq \setminus \approx$$
2		sbthcl	$$⊢\approx =\preccurlyeq \cap {\preccurlyeq }^{-1}$$
3	2	difeq2i	$$⊢\preccurlyeq \setminus \approx =\preccurlyeq \setminus \left(\preccurlyeq \cap {\preccurlyeq }^{-1}\right)$$
4		difin	$$⊢\preccurlyeq \setminus \left(\preccurlyeq \cap {\preccurlyeq }^{-1}\right)=\preccurlyeq \setminus {\preccurlyeq }^{-1}$$
5	1 3 4	3eqtri	$$⊢\prec =\preccurlyeq \setminus {\preccurlyeq }^{-1}$$