Metamath Proof Explorer

Theorem fvn0elsuppb

Description: The function value for a given argument is not empty iff the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 4-Apr-2020)

		Ref	Expression
	Assertion	fvn0elsuppb	$⊢ (B \in V \land X \in B \land G Fn B) \to (G (X) \neq \emptyset \leftrightarrow X \in {supp}_{\emptyset} (G))$

Proof

Step	Hyp	Ref	Expression
1		fvn0elsupp	$⊢ ((B \in V \land X \in B) \land (G Fn B \land G (X) \neq \emptyset)) \to X \in {supp}_{\emptyset} (G)$
2	1	exp43	$⊢ B \in V \to (X \in B \to (G Fn B \to (G (X) \neq \emptyset \to X \in {supp}_{\emptyset} (G))))$
3	2	3imp	$⊢ (B \in V \land X \in B \land G Fn B) \to (G (X) \neq \emptyset \to X \in {supp}_{\emptyset} (G))$
4		simp3	$⊢ (B \in V \land X \in B \land G Fn B) \to G Fn B$
5		simp1	$⊢ (B \in V \land X \in B \land G Fn B) \to B \in V$
6		0ex	$⊢ \emptyset \in V$
7	6	a1i	$⊢ (B \in V \land X \in B \land G Fn B) \to \emptyset \in V$
8		elsuppfn	$⊢ (G Fn B \land B \in V \land \emptyset \in V) \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \neq \emptyset))$
9	4 5 7 8	syl3anc	$⊢ (B \in V \land X \in B \land G Fn B) \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \neq \emptyset))$
10		simpr	$⊢ (X \in B \land G (X) \neq \emptyset) \to G (X) \neq \emptyset$
11	9 10	syl6bi	$⊢ (B \in V \land X \in B \land G Fn B) \to (X \in {supp}_{\emptyset} (G) \to G (X) \neq \emptyset)$
12	3 11	impbid	$⊢ (B \in V \land X \in B \land G Fn B) \to (G (X) \neq \emptyset \leftrightarrow X \in {supp}_{\emptyset} (G))$