Metamath Proof Explorer


Theorem 0fsupp

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

Ref Expression
Assertion 0fsupp ( 𝑍𝑉 → ∅ finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 supp0 ( 𝑍𝑉 → ( ∅ supp 𝑍 ) = ∅ )
2 0fin ∅ ∈ Fin
3 1 2 eqeltrdi ( 𝑍𝑉 → ( ∅ supp 𝑍 ) ∈ Fin )
4 fun0 Fun ∅
5 0ex ∅ ∈ V
6 funisfsupp ( ( Fun ∅ ∧ ∅ ∈ V ∧ 𝑍𝑉 ) → ( ∅ finSupp 𝑍 ↔ ( ∅ supp 𝑍 ) ∈ Fin ) )
7 4 5 6 mp3an12 ( 𝑍𝑉 → ( ∅ finSupp 𝑍 ↔ ( ∅ supp 𝑍 ) ∈ Fin ) )
8 3 7 mpbird ( 𝑍𝑉 → ∅ finSupp 𝑍 )