Metamath Proof Explorer


Theorem frnfsuppbi

Description: Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019)

Ref Expression
Assertion frnfsuppbi ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝐹 : 𝐼𝑆 → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) ) )

Proof

Step Hyp Ref Expression
1 ffun ( 𝐹 : 𝐼𝑆 → Fun 𝐹 )
2 1 adantl ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝐹 : 𝐼𝑆 ) → Fun 𝐹 )
3 fex ( ( 𝐹 : 𝐼𝑆𝐼𝑉 ) → 𝐹 ∈ V )
4 3 expcom ( 𝐼𝑉 → ( 𝐹 : 𝐼𝑆𝐹 ∈ V ) )
5 4 adantr ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝐹 : 𝐼𝑆𝐹 ∈ V ) )
6 5 imp ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝐹 : 𝐼𝑆 ) → 𝐹 ∈ V )
7 simplr ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝐹 : 𝐼𝑆 ) → 𝑍𝑊 )
8 funisfsupp ( ( Fun 𝐹𝐹 ∈ V ∧ 𝑍𝑊 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
9 2 6 7 8 syl3anc ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝐹 : 𝐼𝑆 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
10 frnsuppeq ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝐹 : 𝐼𝑆 → ( 𝐹 supp 𝑍 ) = ( 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) )
11 10 imp ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝐹 : 𝐼𝑆 ) → ( 𝐹 supp 𝑍 ) = ( 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) )
12 11 eleq1d ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝐹 : 𝐼𝑆 ) → ( ( 𝐹 supp 𝑍 ) ∈ Fin ↔ ( 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) )
13 9 12 bitrd ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝐹 : 𝐼𝑆 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) )
14 13 ex ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝐹 : 𝐼𝑆 → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) ) )