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

Metamath Proof Explorer

Theorem fndmfifsupp

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

Ref Expression
Hypotheses fndmfisuppfi.f ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
fndmfisuppfi.d ⊢ ( 𝜑 → 𝐷 ∈ Fin )
fndmfisuppfi.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion fndmfifsupp ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 fndmfisuppfi.f ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
2 fndmfisuppfi.d ⊢ ( 𝜑 → 𝐷 ∈ Fin )
3 fndmfisuppfi.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4 dffn3 ⊢ ( 𝐹 Fn 𝐷 ↔ 𝐹 : 𝐷 ⟶ ran 𝐹 )
5 1 4 sylib ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ran 𝐹 )
6 5 2 3 fdmfifsupp ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )