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	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	fsuppinisegfi.2	⊢ ( 𝜑 → 0 ∈ 𝑊 )
	fsuppinisegfi.3	⊢ ( 𝜑 → 𝑌 ∈ ( V ∖ { 0 } ) )
	fsuppinisegfi.4	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	fsuppinisegfi	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑌 } ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fsuppinisegfi.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		fsuppinisegfi.2	⊢ ( 𝜑 → 0 ∈ 𝑊 )
3		fsuppinisegfi.3	⊢ ( 𝜑 → 𝑌 ∈ ( V ∖ { 0 } ) )
4		fsuppinisegfi.4	⊢ ( 𝜑 → 𝐹 finSupp 0 )
5	4	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
6	3	snssd	⊢ ( 𝜑 → { 𝑌 } ⊆ ( V ∖ { 0 } ) )
7		imass2	⊢ ( { 𝑌 } ⊆ ( V ∖ { 0 } ) → ( ◡ 𝐹 “ { 𝑌 } ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
8	6 7	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑌 } ) ⊆ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
9		suppimacnvss	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ( 𝐹 supp 0 ) )
10	1 2 9	syl2anc	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ( 𝐹 supp 0 ) )
11	8 10	sstrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑌 } ) ⊆ ( 𝐹 supp 0 ) )
12	5 11	ssfid	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑌 } ) ∈ Fin )