sspreima

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

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

Step	Hyp	Ref	Expression
1		inpreima	$⊢ Fun F \to F^{-1} [A \cap B] = F^{-1} [A] \cap F^{-1} [B]$
2		dfss2	$⊢ 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} [A \cap B] = F^{-1} [A]$
5	1 4	sylan9req	$⊢ (Fun F \land A \subseteq B) \to F^{-1} [A] \cap F^{-1} [B] = F^{-1} [A]$
6		dfss2	$⊢ F^{-1} [A] \subseteq F^{-1} [B] \leftrightarrow F^{-1} [A] \cap F^{-1} [B] = F^{-1} [A]$
7	5 6	sylibr	$⊢ (Fun F \land A \subseteq B) \to F^{-1} [A] \subseteq F^{-1} [B]$

Metamath Proof Explorer