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

Metamath Proof Explorer

Theorem cnvimassrndm

Description: The preimage of a superset of the range of a class is the domain of the class. Generalization of cnvimarndm for subsets. (Contributed by AV, 18-Sep-2024)

Ref Expression
Assertion cnvimassrndm ⊢ ran ⁡ F ⊆ A → F -1 A = dom ⁡ F

Proof

Step Hyp Ref Expression
1 ssequn1 ⊢ ran ⁡ F ⊆ A ↔ ran ⁡ F ∪ A = A
2 imaeq2 ⊢ A = ran ⁡ F ∪ A → F -1 A = F -1 ran ⁡ F ∪ A
3 imaundi ⊢ F -1 ran ⁡ F ∪ A = F -1 ran ⁡ F ∪ F -1 A
4 2 3 eqtrdi ⊢ A = ran ⁡ F ∪ A → F -1 A = F -1 ran ⁡ F ∪ F -1 A
5 cnvimarndm ⊢ F -1 ran ⁡ F = dom ⁡ F
6 5 uneq1i ⊢ F -1 ran ⁡ F ∪ F -1 A = dom ⁡ F ∪ F -1 A
7 cnvimass ⊢ F -1 A ⊆ dom ⁡ F
8 ssequn2 ⊢ F -1 A ⊆ dom ⁡ F ↔ dom ⁡ F ∪ F -1 A = dom ⁡ F
9 7 8 mpbi ⊢ dom ⁡ F ∪ F -1 A = dom ⁡ F
10 6 9 eqtri ⊢ F -1 ran ⁡ F ∪ F -1 A = dom ⁡ F
11 4 10 eqtrdi ⊢ A = ran ⁡ F ∪ A → F -1 A = dom ⁡ F
12 11 eqcoms ⊢ ran ⁡ F ∪ A = A → F -1 A = dom ⁡ F
13 1 12 sylbi ⊢ ran ⁡ F ⊆ A → F -1 A = dom ⁡ F