Metamath Proof Explorer


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 )