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 e. V -> ( Rel R -> U. ( dom R /. R ) = ran R ) )

Proof

Step	Hyp	Ref	Expression
1		resexg	|- ( R e. V -> ( R |` dom R ) e. _V )
2		rnresequniqs	|- ( ( R |` dom R ) e. _V -> ran ( R |` dom R ) = U. ( dom R /. R ) )
3	1 2	syl	|- ( R e. V -> ran ( R |` dom R ) = U. ( dom R /. R ) )
4		resdm	|- ( Rel R -> ( R |` dom R ) = R )
5	4	rneqd	|- ( Rel R -> ran ( R |` dom R ) = ran R )
6	3 5	sylan9req	|- ( ( R e. V /\ Rel R ) -> U. ( dom R /. R ) = ran R )
7	6	ex	|- ( R e. V -> ( Rel R -> U. ( dom R /. R ) = ran R ) )