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 
|- ( 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 )