This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )