Theorem dfssr2

Description: Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021)

	Ref	Expression
Assertion	dfssr2	$$⊢\mathrm{S}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\mathrm{E}⋉\left(\mathrm{V}\setminus \mathrm{E}\right)$$

Proof

Step	Hyp	Ref	Expression
1		epel	$$⊢z\mathrm{E}x\leftrightarrow z\in x$$
2		brvdif	$$⊢z\left(\mathrm{V}\setminus \mathrm{E}\right)y\leftrightarrow \neg z\mathrm{E}y$$
3		epel	$$⊢z\mathrm{E}y\leftrightarrow z\in y$$
4	2 3	xchbinx	$$⊢z\left(\mathrm{V}\setminus \mathrm{E}\right)y\leftrightarrow \neg z\in y$$
5	1 4	anbi12i	$$⊢\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\leftrightarrow \left(z\in x\wedge \neg z\in y\right)$$
6	5	exbii	$$⊢\exists z\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\leftrightarrow \exists z\left(z\in x\wedge \neg z\in y\right)$$
7	6	notbii	$$⊢\neg \exists z\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\leftrightarrow \neg \exists z\left(z\in x\wedge \neg z\in y\right)$$
8		dfss6	$$⊢x\subseteq y\leftrightarrow \neg \exists z\left(z\in x\wedge \neg z\in y\right)$$
9	7 8	bitr4i	$$⊢\neg \exists z\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\leftrightarrow x\subseteq y$$
10	9	opabbii	$$⊢\left\{⟨x,y⟩|\neg \exists z\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\right\}=\left\{⟨x,y⟩|x\subseteq y\right\}$$
11		rnxrn	$$⊢\mathrm{ran}\mathrm{E}⋉\left(\mathrm{V}\setminus \mathrm{E}\right)=\left\{⟨x,y⟩|\exists z\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\right\}$$
12	11	difeq2i	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\mathrm{E}⋉\left(\mathrm{V}\setminus \mathrm{E}\right)=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\exists z\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\right\}$$
13		vvdifopab	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left\{⟨x,y⟩|\exists z\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\right\}=\left\{⟨x,y⟩|\neg \exists z\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\right\}$$
14	12 13	eqtri	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\mathrm{E}⋉\left(\mathrm{V}\setminus \mathrm{E}\right)=\left\{⟨x,y⟩|\neg \exists z\left(z\mathrm{E}x\wedge z\left(\mathrm{V}\setminus \mathrm{E}\right)y\right)\right\}$$
15		df-ssr	$$⊢\mathrm{S}=\left\{⟨x,y⟩|x\subseteq y\right\}$$
16	10 14 15	3eqtr4ri	$$⊢\mathrm{S}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\mathrm{E}⋉\left(\mathrm{V}\setminus \mathrm{E}\right)$$