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

Metamath Proof Explorer

Theorem fcdmnn0fsupp

Description: A function into NN0 is finitely supported iff its support is finite. (Contributed by AV, 8-Jul-2019)

Ref Expression
Assertion fcdmnn0fsupp ⊢ I ∈ V ∧ F : I ⟶ ℕ 0 → finSupp 0 ⁡ F ↔ F -1 ℕ ∈ Fin

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 ffsuppbi ⊢ I ∈ V ∧ 0 ∈ V → F : I ⟶ ℕ 0 → finSupp 0 ⁡ F ↔ F -1 ℕ 0 ∖ 0 ∈ Fin
3 1 2 mpan2 ⊢ I ∈ V → F : I ⟶ ℕ 0 → finSupp 0 ⁡ F ↔ F -1 ℕ 0 ∖ 0 ∈ Fin
4 3 imp ⊢ I ∈ V ∧ F : I ⟶ ℕ 0 → finSupp 0 ⁡ F ↔ F -1 ℕ 0 ∖ 0 ∈ Fin
5 dfn2 ⊢ ℕ = ℕ 0 ∖ 0
6 5 imaeq2i ⊢ F -1 ℕ = F -1 ℕ 0 ∖ 0
7 6 eleq1i ⊢ F -1 ℕ ∈ Fin ↔ F -1 ℕ 0 ∖ 0 ∈ Fin
8 4 7 bitr4di ⊢ I ∈ V ∧ F : I ⟶ ℕ 0 → finSupp 0 ⁡ F ↔ F -1 ℕ ∈ Fin