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 )