dfssr2

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

		Ref	Expression
	Assertion	dfssr2	$⊢ S = (V \times V) ∖ ran E ⋉ (V ∖ E)$

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

Metamath Proof Explorer