Metamath Proof Explorer
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 𝑍 ) |