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 φ F V
fsuppinisegfi.2 φ 0 ˙ W
fsuppinisegfi.3 φ Y V 0 ˙
fsuppinisegfi.4 φ finSupp 0 ˙ F
Assertion fsuppinisegfi φ F -1 Y Fin

Proof

Step Hyp Ref Expression
1 fsuppinisegfi.1 φ F V
2 fsuppinisegfi.2 φ 0 ˙ W
3 fsuppinisegfi.3 φ Y V 0 ˙
4 fsuppinisegfi.4 φ finSupp 0 ˙ F
5 4 fsuppimpd φ F supp 0 ˙ Fin
6 3 snssd φ Y V 0 ˙
7 imass2 Y V 0 ˙ F -1 Y F -1 V 0 ˙
8 6 7 syl φ F -1 Y F -1 V 0 ˙
9 suppimacnvss F V 0 ˙ W F -1 V 0 ˙ F supp 0 ˙
10 1 2 9 syl2anc φ F -1 V 0 ˙ F supp 0 ˙
11 8 10 sstrd φ F -1 Y F supp 0 ˙
12 5 11 ssfid φ F -1 Y Fin