suppvalbr

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

		Ref	Expression
	Assertion	suppvalbr	$⊢ (R \in V \land Z \in W) \to R supp Z = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in dom R \| R [\{x\}] \neq \{Z\}\} = \{x \| (x \in dom R \land R [\{x\}] \neq \{Z\})\}$
2		vex	$⊢ x \in V$
3	2	eldm	$⊢ x \in dom R \leftrightarrow \exists y x R y$
4		imasng	$⊢ x \in V \to R [\{x\}] = \{y \| x R y\}$
5	4	elv	$⊢ R [\{x\}] = \{y \| x R y\}$
6	5	neeq1i	$⊢ R [\{x\}] \neq \{Z\} \leftrightarrow \{y \| x R y\} \neq \{Z\}$
7		df-sn	$⊢ \{Z\} = \{y \| y = Z\}$
8	7	neeq2i	$⊢ \{y \| x R y\} \neq \{Z\} \leftrightarrow \{y \| x R y\} \neq \{y \| y = Z\}$
9		nabbib	$⊢ \{y \| x R y\} \neq \{y \| y = Z\} \leftrightarrow \exists y (x R y \leftrightarrow \neg y = Z)$
10	6 8 9	3bitri	$⊢ R [\{x\}] \neq \{Z\} \leftrightarrow \exists y (x R y \leftrightarrow \neg y = Z)$
11	3 10	anbi12i	$⊢ (x \in dom R \land R [\{x\}] \neq \{Z\}) \leftrightarrow (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))$
12	11	abbii	$⊢ \{x \| (x \in dom R \land R [\{x\}] \neq \{Z\})\} = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))\}$
13	1 12	eqtr2i	$⊢ \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))\} = \{x \in dom R \| R [\{x\}] \neq \{Z\}\}$
14	13	a1i	$⊢ (R \in V \land Z \in W) \to \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))\} = \{x \in dom R \| R [\{x\}] \neq \{Z\}\}$
15		df-ne	$⊢ y \neq Z \leftrightarrow \neg y = Z$
16	15	bibi2i	$⊢ (x R y \leftrightarrow y \neq Z) \leftrightarrow (x R y \leftrightarrow \neg y = Z)$
17	16	exbii	$⊢ \exists y (x R y \leftrightarrow y \neq Z) \leftrightarrow \exists y (x R y \leftrightarrow \neg y = Z)$
18	17	anbi2i	$⊢ (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z)) \leftrightarrow (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))$
19	18	abbii	$⊢ \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\} = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))\}$
20	19	a1i	$⊢ (R \in V \land Z \in W) \to \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\} = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))\}$
21		suppval	$⊢ (R \in V \land Z \in W) \to R supp Z = \{x \in dom R \| R [\{x\}] \neq \{Z\}\}$
22	14 20 21	3eqtr4rd	$⊢ (R \in V \land Z \in W) \to R supp Z = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$

Metamath Proof Explorer

Theorem suppvalbr

Proof