Theorem symrelim

Description: Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021)

	Ref	Expression
Assertion	symrelim	$$⊢SymRelR\to \mathrm{dom}R=\mathrm{ran}R$$

Proof

Step	Hyp	Ref	Expression
1		rncnv	$$⊢\mathrm{ran}{R}^{-1}=\mathrm{dom}R$$
2		dfsymrel4	$$⊢SymRelR\leftrightarrow \left(R^{-1}=R\wedge \mathrm{Rel}R\right)$$
3	2	simplbi	$$⊢SymRelR\to R^{-1}=R$$
4	3	rneqd	$$⊢SymRelR\to \mathrm{ran}{R}^{-1}=\mathrm{ran}R$$
5	1 4	syl5eqr	$$⊢SymRelR\to \mathrm{dom}R=\mathrm{ran}R$$