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 C_ A -> ( `' F " A ) = dom F )

Proof

Step Hyp Ref Expression
1 ssequn1 
 |-  ( ran F C_ A <-> ( ran F u. A ) = A )
2 imaeq2 
 |-  ( A = ( ran F u. A ) -> ( `' F " A ) = ( `' F " ( ran F u. A ) ) )
3 imaundi 
 |-  ( `' F " ( ran F u. A ) ) = ( ( `' F " ran F ) u. ( `' F " A ) )
4 2 3 eqtrdi 
 |-  ( A = ( ran F u. A ) -> ( `' F " A ) = ( ( `' F " ran F ) u. ( `' F " A ) ) )
5 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
6 5 uneq1i 
 |-  ( ( `' F " ran F ) u. ( `' F " A ) ) = ( dom F u. ( `' F " A ) )
7 cnvimass 
 |-  ( `' F " A ) C_ dom F
8 ssequn2 
 |-  ( ( `' F " A ) C_ dom F <-> ( dom F u. ( `' F " A ) ) = dom F )
9 7 8 mpbi 
 |-  ( dom F u. ( `' F " A ) ) = dom F
10 6 9 eqtri 
 |-  ( ( `' F " ran F ) u. ( `' F " A ) ) = dom F
11 4 10 eqtrdi 
 |-  ( A = ( ran F u. A ) -> ( `' F " A ) = dom F )
12 11 eqcoms 
 |-  ( ( ran F u. A ) = A -> ( `' F " A ) = dom F )
13 1 12 sylbi 
 |-  ( ran F C_ A -> ( `' F " A ) = dom F )