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	$$⊢\mathrm{ran}F\subseteq A\to F^{-1}\left[A\right]=\mathrm{dom}F$$

Proof

Step	Hyp	Ref	Expression
1		ssequn1	$$⊢\mathrm{ran}F\subseteq A\leftrightarrow \mathrm{ran}F\cup A=A$$
2		imaeq2	$$⊢A=\mathrm{ran}F\cup A\to F^{-1}\left[A\right]=F^{-1}\left[\mathrm{ran}F\cup A\right]$$
3		imaundi	$$⊢F^{-1}\left[\mathrm{ran}F\cup A\right]=F^{-1}\left[\mathrm{ran}F\right]\cup F^{-1}\left[A\right]$$
4	2 3	eqtrdi	$$⊢A=\mathrm{ran}F\cup A\to F^{-1}\left[A\right]=F^{-1}\left[\mathrm{ran}F\right]\cup F^{-1}\left[A\right]$$
5		cnvimarndm	$$⊢F^{-1}\left[\mathrm{ran}F\right]=\mathrm{dom}F$$
6	5	uneq1i	$$⊢F^{-1}\left[\mathrm{ran}F\right]\cup F^{-1}\left[A\right]=\mathrm{dom}F\cup F^{-1}\left[A\right]$$
7		cnvimass	$$⊢F^{-1}\left[A\right]\subseteq \mathrm{dom}F$$
8		ssequn2	$$⊢F^{-1}\left[A\right]\subseteq \mathrm{dom}F\leftrightarrow \mathrm{dom}F\cup F^{-1}\left[A\right]=\mathrm{dom}F$$
9	7 8	mpbi	$$⊢\mathrm{dom}F\cup F^{-1}\left[A\right]=\mathrm{dom}F$$
10	6 9	eqtri	$$⊢F^{-1}\left[\mathrm{ran}F\right]\cup F^{-1}\left[A\right]=\mathrm{dom}F$$
11	4 10	eqtrdi	$$⊢A=\mathrm{ran}F\cup A\to F^{-1}\left[A\right]=\mathrm{dom}F$$
12	11	eqcoms	$$⊢\mathrm{ran}F\cup A=A\to F^{-1}\left[A\right]=\mathrm{dom}F$$
13	1 12	sylbi	$$⊢\mathrm{ran}F\subseteq A\to F^{-1}\left[A\right]=\mathrm{dom}F$$