Theorem unidmqs

Description: The range of a relation is equal to the union of the domain quotient. (Contributed by Peter Mazsa, 13-Oct-2018)

	Ref	Expression
Assertion	unidmqs	$$⊢R\in V\to \left(\mathrm{Rel}R\to \bigcup \left(\mathrm{dom}R/R\right)=\mathrm{ran}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		resexg	$$⊢R\in V\to {R\upharpoonright }_{\mathrm{dom}R}\in \mathrm{V}$$
2		rnresequniqs	$$⊢{R\upharpoonright }_{\mathrm{dom}R}\in \mathrm{V}\to \mathrm{ran}\left({R\upharpoonright }_{\mathrm{dom}R}\right)=\bigcup \left(\mathrm{dom}R/R\right)$$
3	1 2	syl	$$⊢R\in V\to \mathrm{ran}\left({R\upharpoonright }_{\mathrm{dom}R}\right)=\bigcup \left(\mathrm{dom}R/R\right)$$
4		resdm	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\mathrm{dom}R}=R$$
5	4	rneqd	$$⊢\mathrm{Rel}R\to \mathrm{ran}\left({R\upharpoonright }_{\mathrm{dom}R}\right)=\mathrm{ran}R$$
6	3 5	sylan9req	$$⊢\left(R\in V\wedge \mathrm{Rel}R\right)\to \bigcup \left(\mathrm{dom}R/R\right)=\mathrm{ran}R$$
7	6	ex	$$⊢R\in V\to \left(\mathrm{Rel}R\to \bigcup \left(\mathrm{dom}R/R\right)=\mathrm{ran}R\right)$$