imacosupp

Description: The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019)

		Ref	Expression
	Assertion	imacosupp	$⊢ (F \in V \land G \in W) \to ((Fun G \land F supp Z \subseteq ran G) \to G [(F \circ G) supp Z] = F supp Z)$

Step	Hyp	Ref	Expression
1		suppco	$⊢ (F \in V \land G \in W) \to (F \circ G) supp Z = G^{-1} [F supp Z]$
2	1	imaeq2d	$⊢ (F \in V \land G \in W) \to G [(F \circ G) supp Z] = G [G^{-1} [F supp Z]]$
3		funforn	$⊢ Fun G \leftrightarrow G : dom G \underset{onto}{⟶} ran G$
4		foimacnv	$⊢ (G : dom G \underset{onto}{⟶} ran G \land F supp Z \subseteq ran G) \to G [G^{-1} [F supp Z]] = F supp Z$
5	3 4	sylanb	$⊢ (Fun G \land F supp Z \subseteq ran G) \to G [G^{-1} [F supp Z]] = F supp Z$
6	2 5	sylan9eq	$⊢ ((F \in V \land G \in W) \land (Fun G \land F supp Z \subseteq ran G)) \to G [(F \circ G) supp Z] = F supp Z$
7	6	ex	$⊢ (F \in V \land G \in W) \to ((Fun G \land F supp Z \subseteq ran G) \to G [(F \circ G) supp Z] = F supp Z)$

Metamath Proof Explorer