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

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

Metamath Proof Explorer