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

Metamath Proof Explorer

Theorem fdmfifsupp

Description: A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019)

Ref Expression
Hypotheses fdmfisuppfi.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
fdmfisuppfi.d ⊢ ( 𝜑 → 𝐷 ∈ Fin )
fdmfisuppfi.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion fdmfifsupp ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 fdmfisuppfi.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
2 fdmfisuppfi.d ⊢ ( 𝜑 → 𝐷 ∈ Fin )
3 fdmfisuppfi.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4 1 ffund ⊢ ( 𝜑 → Fun 𝐹 )
5 1 2 3 fdmfisuppfi ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
6 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
7 fnex ⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝐷 ∈ Fin ) → 𝐹 ∈ V )
8 6 2 7 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
9 isfsupp ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 ↔ ( Fun 𝐹 ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) ) )
10 8 3 9 syl2anc ⊢ ( 𝜑 → ( 𝐹 finSupp 𝑍 ↔ ( Fun 𝐹 ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) ) )
11 4 5 10 mpbir2and ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )