Metamath Proof Explorer

Theorem 0fsupp

Description: The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019)

Ref Expression
Assertion 0fsupp ⊢ Z ∈ V → finSupp Z⁡ ∅

Proof

Step Hyp Ref Expression
1 supp0 ⊢ Z ∈ V → ∅ supp Z = ∅
2 0fi ⊢ ∅ ∈ Fin
3 1 2 eqeltrdi ⊢ Z ∈ V → ∅ supp Z ∈ Fin
4 fun0 ⊢ Fun ⁡ ∅
5 0ex ⊢ ∅ ∈ V
6 funisfsupp ⊢ Fun ⁡ ∅ ∧ ∅ ∈ V ∧ Z ∈ V → finSupp Z⁡ ∅ ↔ ∅ supp Z ∈ Fin
7 4 5 6 mp3an12 ⊢ Z ∈ V → finSupp Z⁡ ∅ ↔ ∅ supp Z ∈ Fin
8 3 7 mpbird ⊢ Z ∈ V → finSupp Z⁡ ∅