fczfsuppd

Description: A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019)

Step	Hyp	Ref	Expression
1		fczfsuppd.b	$⊢ φ \to B \in V$
2		fczfsuppd.z	$⊢ φ \to Z \in W$
3		fnconstg	$⊢ Z \in W \to (B \times \{Z\}) Fn B$
4		fnfun	$⊢ (B \times \{Z\}) Fn B \to Fun (B \times \{Z\})$
5	2 3 4	3syl	$⊢ φ \to Fun (B \times \{Z\})$
6		fczsupp0	$⊢ (B \times \{Z\}) supp Z = \emptyset$
7		0fin	$⊢ \emptyset \in Fin$
8	6 7	eqeltri	$⊢ (B \times \{Z\}) supp Z \in Fin$
9	8	a1i	$⊢ φ \to (B \times \{Z\}) supp Z \in Fin$
10		snex	$⊢ \{Z\} \in V$
11		xpexg	$⊢ (B \in V \land \{Z\} \in V) \to B \times \{Z\} \in V$
12	1 10 11	sylancl	$⊢ φ \to B \times \{Z\} \in V$
13		isfsupp	$⊢ (B \times \{Z\} \in V \land Z \in W) \to ({finSupp}_{Z} ((B \times \{Z\})) \leftrightarrow (Fun (B \times \{Z\}) \land (B \times \{Z\}) supp Z \in Fin))$
14	12 2 13	syl2anc	$⊢ φ \to ({finSupp}_{Z} ((B \times \{Z\})) \leftrightarrow (Fun (B \times \{Z\}) \land (B \times \{Z\}) supp Z \in Fin))$
15	5 9 14	mpbir2and	$⊢ φ \to {finSupp}_{Z} ((B \times \{Z\}))$

Metamath Proof Explorer