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 )