This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ffsuppbi

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

Ref Expression
Assertion ffsuppbi ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → ( 𝐹 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 fsuppeq ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) )
11 10 imp ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) )
12 11 eleq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( ( 𝐹 supp 𝑍 ) ∈ Fin ↔ ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) )
13 9 12 bitrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( 𝐹 finSupp 𝑍 ↔ ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) )
14 13 ex ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → ( 𝐹 finSupp 𝑍 ↔ ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ∈ Fin ) ) )