Theorem relsdom

Description: Strict dominance is a relation. (Contributed by NM, 31-Mar-1998)

	Ref	Expression
Assertion	relsdom	$$⊢\mathrm{Rel}\prec$$

Proof

Step	Hyp	Ref	Expression
1		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
2		reldif	$$⊢\mathrm{Rel}\preccurlyeq \to \mathrm{Rel}\left(\preccurlyeq \setminus \approx \right)$$
3		df-sdom	$$⊢\prec =\preccurlyeq \setminus \approx$$
4	3	releqi	$$⊢\mathrm{Rel}\prec \leftrightarrow \mathrm{Rel}\left(\preccurlyeq \setminus \approx \right)$$
5	2 4	sylibr	$$⊢\mathrm{Rel}\preccurlyeq \to \mathrm{Rel}\prec$$
6	1 5	ax-mp	$$⊢\mathrm{Rel}\prec$$