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\setminus \left\{Z\right\}$$
Assertion	ffs2	$$⊢\left(A\in V\wedge Z\in W\wedge F:A⟶B\right)\to F\mathrm{supp}Z=F^{-1}\left[C\right]$$

Proof

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