This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ffs2

Description: Rewrite a function's support based with its codomain rather than the universal class. See also fsuppeq . (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

		Ref	Expression
	Hypothesis	ffs2.1	$⊢ C = B ∖ \{Z\}$
	Assertion	ffs2	$⊢ (A \in V \land Z \in W \land F : A ⟶ B) \to F supp Z = F^{-1} [C]$

Proof

Step	Hyp	Ref	Expression
1		ffs2.1	$⊢ C = B ∖ \{Z\}$
2		fsuppeq	$⊢ (A \in V \land Z \in W) \to (F : A ⟶ B \to F supp Z = F^{-1} [B ∖ \{Z\}])$
3	2	3impia	$⊢ (A \in V \land Z \in W \land F : A ⟶ B) \to F supp Z = F^{-1} [B ∖ \{Z\}]$
4	1	imaeq2i	$⊢ F^{-1} [C] = F^{-1} [B ∖ \{Z\}]$
5	3 4	eqtr4di	$⊢ (A \in V \land Z \in W \land F : A ⟶ B) \to F supp Z = F^{-1} [C]$