funimass3

Description: A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv would be the special case of A being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006)

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

Proof

Step	Hyp	Ref	Expression
1		funimass4	$⊢ (Fun F \land A \subseteq dom F) \to (F [A] \subseteq B \leftrightarrow \forall x \in A F (x) \in B)$
2		ssel	$⊢ A \subseteq dom F \to (x \in A \to x \in dom F)$
3		fvimacnv	$⊢ (Fun F \land x \in dom F) \to (F (x) \in B \leftrightarrow x \in F^{-1} [B])$
4	3	ex	$⊢ Fun F \to (x \in dom F \to (F (x) \in B \leftrightarrow x \in F^{-1} [B]))$
5	2 4	syl9r	$⊢ Fun F \to (A \subseteq dom F \to (x \in A \to (F (x) \in B \leftrightarrow x \in F^{-1} [B])))$
6	5	imp31	$⊢ ((Fun F \land A \subseteq dom F) \land x \in A) \to (F (x) \in B \leftrightarrow x \in F^{-1} [B])$
7	6	ralbidva	$⊢ (Fun F \land A \subseteq dom F) \to (\forall x \in A F (x) \in B \leftrightarrow \forall x \in A x \in F^{-1} [B])$
8	1 7	bitrd	$⊢ (Fun F \land A \subseteq dom F) \to (F [A] \subseteq B \leftrightarrow \forall x \in A x \in F^{-1} [B])$
9		dfss3	$⊢ A \subseteq F^{-1} [B] \leftrightarrow \forall x \in A x \in F^{-1} [B]$
10	8 9	bitr4di	$⊢ (Fun F \land A \subseteq dom F) \to (F [A] \subseteq B \leftrightarrow A \subseteq F^{-1} [B])$

Metamath Proof Explorer

Theorem funimass3

Proof