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

Metamath Proof Explorer

Theorem fndmfisuppfi

Description: The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019)

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

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 fdmfisuppfi ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )