Theorem funimass1

Description: A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by NM, 25-May-2004)

	Ref	Expression
Assertion	funimass1	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{ran}F\right)\to \left(F^{-1}\left[A\right]\subseteq B\to A\subseteq F\left[B\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		imass2	$$⊢F^{-1}\left[A\right]\subseteq B\to F\left[F^{-1}\left[A\right]\right]\subseteq F\left[B\right]$$
2		funimacnv	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[A\right]\right]=A\cap \mathrm{ran}F$$
3		dfss	$$⊢A\subseteq \mathrm{ran}F\leftrightarrow A=A\cap \mathrm{ran}F$$
4	3	biimpi	$$⊢A\subseteq \mathrm{ran}F\to A=A\cap \mathrm{ran}F$$
5	4	eqcomd	$$⊢A\subseteq \mathrm{ran}F\to A\cap \mathrm{ran}F=A$$
6	2 5	sylan9eq	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{ran}F\right)\to F\left[F^{-1}\left[A\right]\right]=A$$
7	6	sseq1d	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{ran}F\right)\to \left(F\left[F^{-1}\left[A\right]\right]\subseteq F\left[B\right]\leftrightarrow A\subseteq F\left[B\right]\right)$$
8	1 7	syl5ib	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{ran}F\right)\to \left(F^{-1}\left[A\right]\subseteq B\to A\subseteq F\left[B\right]\right)$$