Theorem funimass2

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

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

Proof

Step	Hyp	Ref	Expression
1		funimacnv	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[B\right]\right]=B\cap \mathrm{ran}F$$
2	1	sseq2d	$$⊢\mathrm{Fun}F\to \left(F\left[A\right]\subseteq F\left[F^{-1}\left[B\right]\right]\leftrightarrow F\left[A\right]\subseteq B\cap \mathrm{ran}F\right)$$
3		inss1	$$⊢B\cap \mathrm{ran}F\subseteq B$$
4		sstr2	$$⊢F\left[A\right]\subseteq B\cap \mathrm{ran}F\to \left(B\cap \mathrm{ran}F\subseteq B\to F\left[A\right]\subseteq B\right)$$
5	3 4	mpi	$$⊢F\left[A\right]\subseteq B\cap \mathrm{ran}F\to F\left[A\right]\subseteq B$$
6	2 5	biimtrdi	$$⊢\mathrm{Fun}F\to \left(F\left[A\right]\subseteq F\left[F^{-1}\left[B\right]\right]\to F\left[A\right]\subseteq B\right)$$
7		imass2	$$⊢A\subseteq F^{-1}\left[B\right]\to F\left[A\right]\subseteq F\left[F^{-1}\left[B\right]\right]$$
8	6 7	impel	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq F^{-1}\left[B\right]\right)\to F\left[A\right]\subseteq B$$