This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ V → Rel ⁡ R → ⋃ dom ⁡ R / R = ran ⁡ R

Proof

Step Hyp Ref Expression
1 resexg ⊢ R ∈ V → R ↾ dom ⁡ R ∈ V
2 rnresequniqs ⊢ R ↾ dom ⁡ R ∈ V → ran ⁡ R ↾ dom ⁡ R = ⋃ dom ⁡ R / R
3 1 2 syl ⊢ R ∈ V → ran ⁡ R ↾ dom ⁡ R = ⋃ 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 ∈ V ∧ Rel ⁡ R → ⋃ dom ⁡ R / R = ran ⁡ R
7 6 ex ⊢ R ∈ V → Rel ⁡ R → ⋃ dom ⁡ R / R = ran ⁡ R