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		suppval	$⊢ (R \in V \land Z \in W) \to R supp Z = \{x \in dom R \| R [\{x\}] \neq \{Z\}\}$
2		df-rab	$⊢ \{x \in dom R \| R [\{x\}] \neq \{Z\}\} = \{x \| (x \in dom R \land R [\{x\}] \neq \{Z\})\}$
3		vex	$⊢ x \in V$
4	3	eldm	$⊢ x \in dom R \leftrightarrow \exists y x R y$
5		df-sn	$⊢ \{Z\} = \{y \| y = Z\}$
6	5	neeq2i	$⊢ \{y \| x R y\} \neq \{Z\} \leftrightarrow \{y \| x R y\} \neq \{y \| y = Z\}$
7		imasng	$⊢ x \in V \to R [\{x\}] = \{y \| x R y\}$
8	7	elv	$⊢ R [\{x\}] = \{y \| x R y\}$
9	8	neeq1i	$⊢ R [\{x\}] \neq \{Z\} \leftrightarrow \{y \| x R y\} \neq \{Z\}$
10		nabbi	$⊢ \exists y (x R y \leftrightarrow \neg y = Z) \leftrightarrow \{y \| x R y\} \neq \{y \| y = Z\}$
11	6 9 10	3bitr4i	$⊢ R [\{x\}] \neq \{Z\} \leftrightarrow \exists y (x R y \leftrightarrow \neg y = Z)$
12	4 11	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))$
13	12	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))\}$
14	2 13	eqtri	$⊢ \{x \in dom R \| R [\{x\}] \neq \{Z\}\} = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))\}$
15	14	a1i	$⊢ (R \in V \land Z \in W) \to \{x \in dom R \| R [\{x\}] \neq \{Z\}\} = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))\}$
16		df-ne	$⊢ y \neq Z \leftrightarrow \neg y = Z$
17	16	bicomi	$⊢ \neg y = Z \leftrightarrow y \neq Z$
18	17	bibi2i	$⊢ (x R y \leftrightarrow \neg y = Z) \leftrightarrow (x R y \leftrightarrow y \neq Z)$
19	18	exbii	$⊢ \exists y (x R y \leftrightarrow \neg y = Z) \leftrightarrow \exists y (x R y \leftrightarrow y \neq Z)$
20	19	anbi2i	$⊢ (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z)) \leftrightarrow (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))$
21	20	abbii	$⊢ \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow \neg y = Z))\} = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$
22	21	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 \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$
23	1 15 22	3eqtrd	$⊢ (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