Metamath Proof Explorer

Theorem fcdmnn0fsuppg

Description: Version of fcdmnn0fsupp avoiding ax-rep by assuming F is a set rather than its domain I . (Contributed by SN, 5-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 ffun ⊢ F : I ⟶ ℕ 0 → Fun ⁡ F
2 simpl ⊢ F ∈ V ∧ F : I ⟶ ℕ 0 → F ∈ V
3 c0ex ⊢ 0 ∈ V
4 funisfsupp ⊢ Fun ⁡ F ∧ F ∈ V ∧ 0 ∈ V → finSupp 0 ⁡ F ↔ F supp 0 ∈ Fin
5 3 4 mp3an3 ⊢ Fun ⁡ F ∧ F ∈ V → finSupp 0 ⁡ F ↔ F supp 0 ∈ Fin
6 1 2 5 syl2an2 ⊢ F ∈ V ∧ F : I ⟶ ℕ 0 → finSupp 0 ⁡ F ↔ F supp 0 ∈ Fin
7 fcdmnn0suppg ⊢ F ∈ V ∧ F : I ⟶ ℕ 0 → F supp 0 = F -1 ℕ
8 7 eleq1d ⊢ F ∈ V ∧ F : I ⟶ ℕ 0 → F supp 0 ∈ Fin ↔ F -1 ℕ ∈ Fin
9 6 8 bitrd ⊢ F ∈ V ∧ F : I ⟶ ℕ 0 → finSupp 0 ⁡ F ↔ F -1 ℕ ∈ Fin