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		0fi	⊢ ∅ ∈ 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 𝑍 )