Metamath Proof Explorer

Theorem fsupprnfi

Description: Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024)

Ref Expression
Assertion fsupprnfi ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ran 𝐹 ∈ Fin )

Proof

Step Hyp Ref Expression
1 snfi ⊢ { 0 } ∈ Fin
2 simpll ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → Fun 𝐹 )
3 simplr ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → 𝐹 ∈ 𝑉 )
4 simprl ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → 0 ∈ 𝑊 )
5 ressupprn ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊 ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) )
6 2 3 4 5 syl3anc ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) )
7 simprr ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → 𝐹 finSupp 0 )
8 7 fsuppimpd ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 supp 0 ) ∈ Fin )
9 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
10 ssdmres ⊢ ( ( 𝐹 supp 0 ) ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) )
11 9 10 mpbi ⊢ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 )
12 2 funresd ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
13 funforn ⊢ ( Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
14 12 13 sylib ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
15 foeq2 ⊢ ( dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) → ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : ( 𝐹 supp 0 ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) )
16 15 biimpa ⊢ ( ( dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) ∧ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : ( 𝐹 supp 0 ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
17 11 14 16 sylancr ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : ( 𝐹 supp 0 ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
18 fofi ⊢ ( ( ( 𝐹 supp 0 ) ∈ Fin ∧ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) : ( 𝐹 supp 0 ) –onto→ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
19 8 17 18 syl2anc ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
20 6 19 eqeltrrd ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
21 diffib ⊢ ( { 0 } ∈ Fin → ( ran 𝐹 ∈ Fin ↔ ( ran 𝐹 ∖ { 0 } ) ∈ Fin ) )
22 21 biimpar ⊢ ( ( { 0 } ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ∈ Fin ) → ran 𝐹 ∈ Fin )
23 1 20 22 sylancr ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 ) ) → ran 𝐹 ∈ Fin )