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

Metamath Proof Explorer

Theorem fidmfisupp

Description: A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses fidmfisupp.1 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
fidmfisupp.2 ⊢ ( 𝜑 → 𝐷 ∈ Fin )
fidmfisupp.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion fidmfisupp ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 fidmfisupp.1 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
2 fidmfisupp.2 ⊢ ( 𝜑 → 𝐷 ∈ Fin )
3 fidmfisupp.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4 1 2 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
5 suppimacnv ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
6 4 3 5 syl2anc ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
7 2 1 fisuppfi ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
8 6 7 eqeltrd ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
9 1 ffund ⊢ ( 𝜑 → Fun 𝐹 )
10 funisfsupp ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
11 9 4 3 10 syl3anc ⊢ ( 𝜑 → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
12 8 11 mpbird ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )