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	⊢ ( 𝑅 ∈ 𝑉 → ( Rel 𝑅 → ∪ ( dom 𝑅 / 𝑅 ) = ran 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		resexg	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↾ dom 𝑅 ) ∈ V )
2		rnresequniqs	⊢ ( ( 𝑅 ↾ dom 𝑅 ) ∈ V → ran ( 𝑅 ↾ dom 𝑅 ) = ∪ ( dom 𝑅 / 𝑅 ) )
3	1 2	syl	⊢ ( 𝑅 ∈ 𝑉 → ran ( 𝑅 ↾ dom 𝑅 ) = ∪ ( dom 𝑅 / 𝑅 ) )
4		resdm	⊢ ( Rel 𝑅 → ( 𝑅 ↾ dom 𝑅 ) = 𝑅 )
5	4	rneqd	⊢ ( Rel 𝑅 → ran ( 𝑅 ↾ dom 𝑅 ) = ran 𝑅 )
6	3 5	sylan9req	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ∪ ( dom 𝑅 / 𝑅 ) = ran 𝑅 )
7	6	ex	⊢ ( 𝑅 ∈ 𝑉 → ( Rel 𝑅 → ∪ ( dom 𝑅 / 𝑅 ) = ran 𝑅 ) )