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	$⊢ (Fun F \land A \subseteq ran F) \to (F^{-1} [A] \subseteq B \to A \subseteq F [B])$

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

Metamath Proof Explorer