Metamath Proof Explorer

Theorem fnsuppeq0

Description: The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015) (Revised by AV, 28-May-2019)

		Ref	Expression
	Assertion	fnsuppeq0	$⊢ (F Fn A \land A \in W \land Z \in V) \to (F supp Z = \emptyset \leftrightarrow F = A \times \{Z\})$

Proof

Step	Hyp	Ref	Expression
1		ss0b	$⊢ F supp Z \subseteq \emptyset \leftrightarrow F supp Z = \emptyset$
2		un0	$⊢ A \cup \emptyset = A$
3		uncom	$⊢ A \cup \emptyset = \emptyset \cup A$
4	2 3	eqtr3i	$⊢ A = \emptyset \cup A$
5	4	fneq2i	$⊢ F Fn A \leftrightarrow F Fn (\emptyset \cup A)$
6	5	biimpi	$⊢ F Fn A \to F Fn (\emptyset \cup A)$
7	6	3ad2ant1	$⊢ (F Fn A \land A \in W \land Z \in V) \to F Fn (\emptyset \cup A)$
8		fnex	$⊢ (F Fn A \land A \in W) \to F \in V$
9	8	3adant3	$⊢ (F Fn A \land A \in W \land Z \in V) \to F \in V$
10		simp3	$⊢ (F Fn A \land A \in W \land Z \in V) \to Z \in V$
11		0in	$⊢ \emptyset \cap A = \emptyset$
12	11	a1i	$⊢ (F Fn A \land A \in W \land Z \in V) \to \emptyset \cap A = \emptyset$
13		fnsuppres	$⊢ (F Fn (\emptyset \cup A) \land (F \in V \land Z \in V) \land \emptyset \cap A = \emptyset) \to (F supp Z \subseteq \emptyset \leftrightarrow {F ↾}_{A} = A \times \{Z\})$
14	7 9 10 12 13	syl121anc	$⊢ (F Fn A \land A \in W \land Z \in V) \to (F supp Z \subseteq \emptyset \leftrightarrow {F ↾}_{A} = A \times \{Z\})$
15	1 14	bitr3id	$⊢ (F Fn A \land A \in W \land Z \in V) \to (F supp Z = \emptyset \leftrightarrow {F ↾}_{A} = A \times \{Z\})$
16		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
17	16	3ad2ant1	$⊢ (F Fn A \land A \in W \land Z \in V) \to {F ↾}_{A} = F$
18	17	eqeq1d	$⊢ (F Fn A \land A \in W \land Z \in V) \to ({F ↾}_{A} = A \times \{Z\} \leftrightarrow F = A \times \{Z\})$
19	15 18	bitrd	$⊢ (F Fn A \land A \in W \land Z \in V) \to (F supp Z = \emptyset \leftrightarrow F = A \times \{Z\})$