fczsupp0

Description: The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019)

		Ref	Expression
	Assertion	fczsupp0	$⊢ (B \times \{Z\}) supp Z = \emptyset$

Step	Hyp	Ref	Expression
1		eqidd	$⊢ (B \times \{Z\} \in V \land Z \in V) \to B \times \{Z\} = B \times \{Z\}$
2		fnconstg	$⊢ Z \in V \to (B \times \{Z\}) Fn B$
3	2	adantl	$⊢ (B \times \{Z\} \in V \land Z \in V) \to (B \times \{Z\}) Fn B$
4		snnzg	$⊢ Z \in V \to \{Z\} \neq \emptyset$
5		simpl	$⊢ (B \times \{Z\} \in V \land Z \in V) \to B \times \{Z\} \in V$
6		xpexcnv	$⊢ (\{Z\} \neq \emptyset \land B \times \{Z\} \in V) \to B \in V$
7	4 5 6	syl2an2	$⊢ (B \times \{Z\} \in V \land Z \in V) \to B \in V$
8		simpr	$⊢ (B \times \{Z\} \in V \land Z \in V) \to Z \in V$
9		fnsuppeq0	$⊢ ((B \times \{Z\}) Fn B \land B \in V \land Z \in V) \to ((B \times \{Z\}) supp Z = \emptyset \leftrightarrow B \times \{Z\} = B \times \{Z\})$
10	3 7 8 9	syl3anc	$⊢ (B \times \{Z\} \in V \land Z \in V) \to ((B \times \{Z\}) supp Z = \emptyset \leftrightarrow B \times \{Z\} = B \times \{Z\})$
11	1 10	mpbird	$⊢ (B \times \{Z\} \in V \land Z \in V) \to (B \times \{Z\}) supp Z = \emptyset$
12		supp0prc	$⊢ \neg (B \times \{Z\} \in V \land Z \in V) \to (B \times \{Z\}) supp Z = \emptyset$
13	11 12	pm2.61i	$⊢ (B \times \{Z\}) supp Z = \emptyset$

Metamath Proof Explorer