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 e. V -> (/) finSupp Z )

Proof

Step Hyp Ref Expression
1 supp0
 |-  ( Z e. V -> ( (/) supp Z ) = (/) )
2 0fin
 |-  (/) e. Fin
3 1 2 eqeltrdi
 |-  ( Z e. V -> ( (/) supp Z ) e. Fin )
4 fun0
 |-  Fun (/)
5 0ex
 |-  (/) e. _V
6 funisfsupp
 |-  ( ( Fun (/) /\ (/) e. _V /\ Z e. V ) -> ( (/) finSupp Z <-> ( (/) supp Z ) e. Fin ) )
7 4 5 6 mp3an12
 |-  ( Z e. V -> ( (/) finSupp Z <-> ( (/) supp Z ) e. Fin ) )
8 3 7 mpbird
 |-  ( Z e. V -> (/) finSupp Z )