0fsupp

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

		Ref	Expression
	Assertion	0fsupp	$⊢ Z \in V \to {finSupp}_{Z} (\emptyset)$

Step	Hyp	Ref	Expression
1		supp0	$⊢ Z \in V \to \emptyset supp Z = \emptyset$
2		0fi	$⊢ \emptyset \in Fin$
3	1 2	eqeltrdi	$⊢ Z \in V \to \emptyset supp Z \in Fin$
4		fun0	$⊢ Fun \emptyset$
5		0ex	$⊢ \emptyset \in V$
6		funisfsupp	$⊢ (Fun \emptyset \land \emptyset \in V \land Z \in V) \to ({finSupp}_{Z} (\emptyset) \leftrightarrow \emptyset supp Z \in Fin)$
7	4 5 6	mp3an12	$⊢ Z \in V \to ({finSupp}_{Z} (\emptyset) \leftrightarrow \emptyset supp Z \in Fin)$
8	3 7	mpbird	$⊢ Z \in V \to {finSupp}_{Z} (\emptyset)$

Metamath Proof Explorer