suppval

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

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

Step	Hyp	Ref	Expression
1		df-supp	$⊢ supp = (x \in V, z \in V ⟼ \{i \in dom x \| x [\{i\}] \neq \{z\}\})$
2	1	a1i	$⊢ (X \in V \land Z \in W) \to supp = (x \in V, z \in V ⟼ \{i \in dom x \| x [\{i\}] \neq \{z\}\})$
3		dmeq	$⊢ x = X \to dom x = dom X$
4	3	adantr	$⊢ (x = X \land z = Z) \to dom x = dom X$
5		imaeq1	$⊢ x = X \to x [\{i\}] = X [\{i\}]$
6	5	adantr	$⊢ (x = X \land z = Z) \to x [\{i\}] = X [\{i\}]$
7		sneq	$⊢ z = Z \to \{z\} = \{Z\}$
8	7	adantl	$⊢ (x = X \land z = Z) \to \{z\} = \{Z\}$
9	6 8	neeq12d	$⊢ (x = X \land z = Z) \to (x [\{i\}] \neq \{z\} \leftrightarrow X [\{i\}] \neq \{Z\})$
10	4 9	rabeqbidv	$⊢ (x = X \land z = Z) \to \{i \in dom x \| x [\{i\}] \neq \{z\}\} = \{i \in dom X \| X [\{i\}] \neq \{Z\}\}$
11	10	adantl	$⊢ ((X \in V \land Z \in W) \land (x = X \land z = Z)) \to \{i \in dom x \| x [\{i\}] \neq \{z\}\} = \{i \in dom X \| X [\{i\}] \neq \{Z\}\}$
12		elex	$⊢ X \in V \to X \in V$
13	12	adantr	$⊢ (X \in V \land Z \in W) \to X \in V$
14		elex	$⊢ Z \in W \to Z \in V$
15	14	adantl	$⊢ (X \in V \land Z \in W) \to Z \in V$
16		dmexg	$⊢ X \in V \to dom X \in V$
17	16	adantr	$⊢ (X \in V \land Z \in W) \to dom X \in V$
18		rabexg	$⊢ dom X \in V \to \{i \in dom X \| X [\{i\}] \neq \{Z\}\} \in V$
19	17 18	syl	$⊢ (X \in V \land Z \in W) \to \{i \in dom X \| X [\{i\}] \neq \{Z\}\} \in V$
20	2 11 13 15 19	ovmpod	$⊢ (X \in V \land Z \in W) \to X supp Z = \{i \in dom X \| X [\{i\}] \neq \{Z\}\}$

Metamath Proof Explorer