suppval1

Description: The value of the operation constructing the support of a function. (Contributed by AV, 6-Apr-2019)

		Ref	Expression
	Assertion	suppval1	$⊢ (Fun X \land X \in V \land Z \in W) \to X supp Z = \{i \in dom X \| X (i) \neq Z\}$

Step	Hyp	Ref	Expression
1		suppval	$⊢ (X \in V \land Z \in W) \to X supp Z = \{i \in dom X \| X [\{i\}] \neq \{Z\}\}$
2	1	3adant1	$⊢ (Fun X \land X \in V \land Z \in W) \to X supp Z = \{i \in dom X \| X [\{i\}] \neq \{Z\}\}$
3		funfn	$⊢ Fun X \leftrightarrow X Fn dom X$
4	3	biimpi	$⊢ Fun X \to X Fn dom X$
5	4	3ad2ant1	$⊢ (Fun X \land X \in V \land Z \in W) \to X Fn dom X$
6		fnsnfv	$⊢ (X Fn dom X \land i \in dom X) \to \{X (i)\} = X [\{i\}]$
7	5 6	sylan	$⊢ ((Fun X \land X \in V \land Z \in W) \land i \in dom X) \to \{X (i)\} = X [\{i\}]$
8	7	eqcomd	$⊢ ((Fun X \land X \in V \land Z \in W) \land i \in dom X) \to X [\{i\}] = \{X (i)\}$
9	8	neeq1d	$⊢ ((Fun X \land X \in V \land Z \in W) \land i \in dom X) \to (X [\{i\}] \neq \{Z\} \leftrightarrow \{X (i)\} \neq \{Z\})$
10		fvex	$⊢ X (i) \in V$
11		sneqbg	$⊢ X (i) \in V \to (\{X (i)\} = \{Z\} \leftrightarrow X (i) = Z)$
12	10 11	mp1i	$⊢ ((Fun X \land X \in V \land Z \in W) \land i \in dom X) \to (\{X (i)\} = \{Z\} \leftrightarrow X (i) = Z)$
13	12	necon3bid	$⊢ ((Fun X \land X \in V \land Z \in W) \land i \in dom X) \to (\{X (i)\} \neq \{Z\} \leftrightarrow X (i) \neq Z)$
14	9 13	bitrd	$⊢ ((Fun X \land X \in V \land Z \in W) \land i \in dom X) \to (X [\{i\}] \neq \{Z\} \leftrightarrow X (i) \neq Z)$
15	14	rabbidva	$⊢ (Fun X \land X \in V \land Z \in W) \to \{i \in dom X \| X [\{i\}] \neq \{Z\}\} = \{i \in dom X \| X (i) \neq Z\}$
16	2 15	eqtrd	$⊢ (Fun X \land X \in V \land Z \in W) \to X supp Z = \{i \in dom X \| X (i) \neq Z\}$

Metamath Proof Explorer