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)

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

Metamath Proof Explorer