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 𝑍 )