Theorem fsuppinisegfi

Description: The initial segment (`' F " { Y } ) of a nonzero Y is finite if F ` has finite support. (Contributed by Thierry Arnoux, 21-Jun-2024)

	Ref	Expression
Hypotheses	fsuppinisegfi.1	$$⊢\phi \to F\in V$$
	fsuppinisegfi.2	$$⊢\phi \to \underset{\dot{}}{0}\in W$$
	fsuppinisegfi.3	$$⊢\phi \to Y\in \left(\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	fsuppinisegfi.4	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	fsuppinisegfi	$$⊢\phi \to F^{-1}\left[\left\{Y\right\}\right]\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		fsuppinisegfi.1	$$⊢\phi \to F\in V$$
2		fsuppinisegfi.2	$$⊢\phi \to \underset{\dot{}}{0}\in W$$
3		fsuppinisegfi.3	$$⊢\phi \to Y\in \left(\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
4		fsuppinisegfi.4	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
5	4	fsuppimpd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
6	3	snssd	$$⊢\phi \to \left\{Y\right\}\subseteq \mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}$$
7		imass2	$$⊢\left\{Y\right\}\subseteq \mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\to F^{-1}\left[\left\{Y\right\}\right]\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
8	6 7	syl	$$⊢\phi \to F^{-1}\left[\left\{Y\right\}\right]\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
9		suppimacnvss	$$⊢\left(F\in V\wedge \underset{\dot{}}{0}\in W\right)\to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
10	1 2 9	syl2anc	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
11	8 10	sstrd	$$⊢\phi \to F^{-1}\left[\left\{Y\right\}\right]\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
12	5 11	ssfid	$$⊢\phi \to F^{-1}\left[\left\{Y\right\}\right]\in \mathrm{Fin}$$