Theorem cnvimainrn

Description: The preimage of the intersection of the range of a class and a class A is the preimage of the class A . (Contributed by AV, 17-Sep-2024)

	Ref	Expression
Assertion	cnvimainrn	$$⊢\mathrm{Fun}F\to F^{-1}\left[\mathrm{ran}F\cap A\right]=F^{-1}\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		inpreima	$$⊢\mathrm{Fun}F\to F^{-1}\left[\mathrm{ran}F\cap A\right]=F^{-1}\left[\mathrm{ran}F\right]\cap F^{-1}\left[A\right]$$
2		cnvimass	$$⊢F^{-1}\left[A\right]\subseteq \mathrm{dom}F$$
3		cnvimarndm	$$⊢F^{-1}\left[\mathrm{ran}F\right]=\mathrm{dom}F$$
4	2 3	sseqtrri	$$⊢F^{-1}\left[A\right]\subseteq F^{-1}\left[\mathrm{ran}F\right]$$
5		dfss2	$$⊢F^{-1}\left[A\right]\subseteq F^{-1}\left[\mathrm{ran}F\right]\leftrightarrow F^{-1}\left[A\right]\cap F^{-1}\left[\mathrm{ran}F\right]=F^{-1}\left[A\right]$$
6	4 5	mpbi	$$⊢F^{-1}\left[A\right]\cap F^{-1}\left[\mathrm{ran}F\right]=F^{-1}\left[A\right]$$
7	6	ineqcomi	$$⊢F^{-1}\left[\mathrm{ran}F\right]\cap F^{-1}\left[A\right]=F^{-1}\left[A\right]$$
8	1 7	eqtrdi	$$⊢\mathrm{Fun}F\to F^{-1}\left[\mathrm{ran}F\cap A\right]=F^{-1}\left[A\right]$$