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 0fin 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