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 | ⊢ ( 𝑅 ∈ 𝑉 → ( Rel 𝑅 → ( ( dom 𝑅 / 𝑅 ) = 𝐴 → ran 𝑅 = ∪ 𝐴 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unieq | ⊢ ( ( dom 𝑅 / 𝑅 ) = 𝐴 → ∪ ( dom 𝑅 / 𝑅 ) = ∪ 𝐴 ) | |
| 2 | unidmqseq | ⊢ ( 𝑅 ∈ 𝑉 → ( Rel 𝑅 → ( ∪ ( dom 𝑅 / 𝑅 ) = ∪ 𝐴 ↔ ran 𝑅 = ∪ 𝐴 ) ) ) | |
| 3 | 2 | imp | ⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( ∪ ( dom 𝑅 / 𝑅 ) = ∪ 𝐴 ↔ ran 𝑅 = ∪ 𝐴 ) ) |
| 4 | 1 3 | imbitrid | ⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( ( dom 𝑅 / 𝑅 ) = 𝐴 → ran 𝑅 = ∪ 𝐴 ) ) |
| 5 | 4 | ex | ⊢ ( 𝑅 ∈ 𝑉 → ( Rel 𝑅 → ( ( dom 𝑅 / 𝑅 ) = 𝐴 → ran 𝑅 = ∪ 𝐴 ) ) ) |