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 )