Theorem dmqseqim

Description: If the domain quotient of a relation is equal to the class A , then the range of the relation is the union of the class. (Contributed by Peter Mazsa, 29-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		unieq	$$⊢\mathrm{dom}R/R=A\to \bigcup \left(\mathrm{dom}R/R\right)=\bigcup A$$
2		unidmqseq	$$⊢R\in V\to \left(\mathrm{Rel}R\to \left(\bigcup \left(\mathrm{dom}R/R\right)=\bigcup A\leftrightarrow \mathrm{ran}R=\bigcup A\right)\right)$$
3	2	imp	$$⊢\left(R\in V\wedge \mathrm{Rel}R\right)\to \left(\bigcup \left(\mathrm{dom}R/R\right)=\bigcup A\leftrightarrow \mathrm{ran}R=\bigcup A\right)$$
4	1 3	syl5ib	$$⊢\left(R\in V\wedge \mathrm{Rel}R\right)\to \left(\mathrm{dom}R/R=A\to \mathrm{ran}R=\bigcup A\right)$$
5	4	ex	$$⊢R\in V\to \left(\mathrm{Rel}R\to \left(\mathrm{dom}R/R=A\to \mathrm{ran}R=\bigcup A\right)\right)$$