Theorem sspreima

Description: The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017)

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

Proof

Step	Hyp	Ref	Expression
1		inpreima	$$⊢\mathrm{Fun}F\to F^{-1}\left[A\cap B\right]=F^{-1}\left[A\right]\cap F^{-1}\left[B\right]$$
2		df-ss	$$⊢A\subseteq B\leftrightarrow A\cap B=A$$
3	2	biimpi	$$⊢A\subseteq B\to A\cap B=A$$
4	3	imaeq2d	$$⊢A\subseteq B\to F^{-1}\left[A\cap B\right]=F^{-1}\left[A\right]$$
5	1 4	sylan9req	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq B\right)\to F^{-1}\left[A\right]\cap F^{-1}\left[B\right]=F^{-1}\left[A\right]$$
6		df-ss	$$⊢F^{-1}\left[A\right]\subseteq F^{-1}\left[B\right]\leftrightarrow F^{-1}\left[A\right]\cap F^{-1}\left[B\right]=F^{-1}\left[A\right]$$
7	5 6	sylibr	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq B\right)\to F^{-1}\left[A\right]\subseteq F^{-1}\left[B\right]$$