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 𝐹 ⊆ 𝐴 → ( ◡ 𝐹 “ 𝐴 ) = dom 𝐹 )

Proof

Step Hyp Ref Expression
1 ssequn1 ⊢ ( ran 𝐹 ⊆ 𝐴 ↔ ( ran 𝐹 ∪ 𝐴 ) = 𝐴 )
2 imaeq2 ⊢ ( 𝐴 = ( ran 𝐹 ∪ 𝐴 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( ran 𝐹 ∪ 𝐴 ) ) )
3 imaundi ⊢ ( ◡ 𝐹 “ ( ran 𝐹 ∪ 𝐴 ) ) = ( ( ◡ 𝐹 “ ran 𝐹 ) ∪ ( ◡ 𝐹 “ 𝐴 ) )
4 2 3 eqtrdi ⊢ ( 𝐴 = ( ran 𝐹 ∪ 𝐴 ) → ( ◡ 𝐹 “ 𝐴 ) = ( ( ◡ 𝐹 “ ran 𝐹 ) ∪ ( ◡ 𝐹 “ 𝐴 ) ) )
5 cnvimarndm ⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
6 5 uneq1i ⊢ ( ( ◡ 𝐹 “ ran 𝐹 ) ∪ ( ◡ 𝐹 “ 𝐴 ) ) = ( dom 𝐹 ∪ ( ◡ 𝐹 “ 𝐴 ) )
7 cnvimass ⊢ ( ◡ 𝐹 “ 𝐴 ) ⊆ dom 𝐹
8 ssequn2 ⊢ ( ( ◡ 𝐹 “ 𝐴 ) ⊆ dom 𝐹 ↔ ( dom 𝐹 ∪ ( ◡ 𝐹 “ 𝐴 ) ) = dom 𝐹 )
9 7 8 mpbi ⊢ ( dom 𝐹 ∪ ( ◡ 𝐹 “ 𝐴 ) ) = dom 𝐹
10 6 9 eqtri ⊢ ( ( ◡ 𝐹 “ ran 𝐹 ) ∪ ( ◡ 𝐹 “ 𝐴 ) ) = dom 𝐹
11 4 10 eqtrdi ⊢ ( 𝐴 = ( ran 𝐹 ∪ 𝐴 ) → ( ◡ 𝐹 “ 𝐴 ) = dom 𝐹 )
12 11 eqcoms ⊢ ( ( ran 𝐹 ∪ 𝐴 ) = 𝐴 → ( ◡ 𝐹 “ 𝐴 ) = dom 𝐹 )
13 1 12 sylbi ⊢ ( ran 𝐹 ⊆ 𝐴 → ( ◡ 𝐹 “ 𝐴 ) = dom 𝐹 )