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	|- ( ph -> F e. V )
	fsuppinisegfi.2	|- ( ph -> .0. e. W )
	fsuppinisegfi.3	|- ( ph -> Y e. ( _V \ { .0. } ) )
	fsuppinisegfi.4	|- ( ph -> F finSupp .0. )
Assertion	fsuppinisegfi	|- ( ph -> ( `' F " { Y } ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		fsuppinisegfi.1	|- ( ph -> F e. V )
2		fsuppinisegfi.2	|- ( ph -> .0. e. W )
3		fsuppinisegfi.3	|- ( ph -> Y e. ( _V \ { .0. } ) )
4		fsuppinisegfi.4	|- ( ph -> F finSupp .0. )
5	4	fsuppimpd	|- ( ph -> ( F supp .0. ) e. Fin )
6	3	snssd	|- ( ph -> { Y } C_ ( _V \ { .0. } ) )
7		imass2	|- ( { Y } C_ ( _V \ { .0. } ) -> ( `' F " { Y } ) C_ ( `' F " ( _V \ { .0. } ) ) )
8	6 7	syl	|- ( ph -> ( `' F " { Y } ) C_ ( `' F " ( _V \ { .0. } ) ) )
9		suppimacnvss	|- ( ( F e. V /\ .0. e. W ) -> ( `' F " ( _V \ { .0. } ) ) C_ ( F supp .0. ) )
10	1 2 9	syl2anc	|- ( ph -> ( `' F " ( _V \ { .0. } ) ) C_ ( F supp .0. ) )
11	8 10	sstrd	|- ( ph -> ( `' F " { Y } ) C_ ( F supp .0. ) )
12	5 11	ssfid	|- ( ph -> ( `' F " { Y } ) e. Fin )