dfsup2

Description: Quantifier-free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013)

		Ref	Expression
	Assertion	dfsup2	$⊢ sup (B, A, R) = ⋃ (A ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]]))$

Proof

Step	Hyp	Ref	Expression
1		df-sup	$⊢ sup (B, A, R) = ⋃ \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\}$
2		dfrab3	$⊢ \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} = A \cap \{x \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\}$
3		eqabcb	$⊢ \{x \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} = V ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]]) \leftrightarrow \forall x ((\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \leftrightarrow x \in (V ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])))$
4		vex	$⊢ x \in V$
5		eldif	$⊢ x \in (V ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])) \leftrightarrow (x \in V \land \neg x \in (R^{-1} [B] \cup R [A ∖ R^{-1} [B]]))$
6	4 5	mpbiran	$⊢ x \in (V ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])) \leftrightarrow \neg x \in (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])$
7	4	elima	$⊢ x \in R^{-1} [B] \leftrightarrow \exists y \in B y R^{-1} x$
8		dfrex2	$⊢ \exists y \in B y R^{-1} x \leftrightarrow \neg \forall y \in B \neg y R^{-1} x$
9	7 8	bitri	$⊢ x \in R^{-1} [B] \leftrightarrow \neg \forall y \in B \neg y R^{-1} x$
10	4	elima	$⊢ x \in R [A ∖ R^{-1} [B]] \leftrightarrow \exists y \in (A ∖ R^{-1} [B]) y R x$
11		dfrex2	$⊢ \exists y \in (A ∖ R^{-1} [B]) y R x \leftrightarrow \neg \forall y \in (A ∖ R^{-1} [B]) \neg y R x$
12	10 11	bitri	$⊢ x \in R [A ∖ R^{-1} [B]] \leftrightarrow \neg \forall y \in (A ∖ R^{-1} [B]) \neg y R x$
13	9 12	orbi12i	$⊢ (x \in R^{-1} [B] \lor x \in R [A ∖ R^{-1} [B]]) \leftrightarrow (\neg \forall y \in B \neg y R^{-1} x \lor \neg \forall y \in (A ∖ R^{-1} [B]) \neg y R x)$
14		elun	$⊢ x \in (R^{-1} [B] \cup R [A ∖ R^{-1} [B]]) \leftrightarrow (x \in R^{-1} [B] \lor x \in R [A ∖ R^{-1} [B]])$
15		ianor	$⊢ \neg (\forall y \in B \neg y R^{-1} x \land \forall y \in (A ∖ R^{-1} [B]) \neg y R x) \leftrightarrow (\neg \forall y \in B \neg y R^{-1} x \lor \neg \forall y \in (A ∖ R^{-1} [B]) \neg y R x)$
16	13 14 15	3bitr4i	$⊢ x \in (R^{-1} [B] \cup R [A ∖ R^{-1} [B]]) \leftrightarrow \neg (\forall y \in B \neg y R^{-1} x \land \forall y \in (A ∖ R^{-1} [B]) \neg y R x)$
17	16	con2bii	$⊢ (\forall y \in B \neg y R^{-1} x \land \forall y \in (A ∖ R^{-1} [B]) \neg y R x) \leftrightarrow \neg x \in (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])$
18		vex	$⊢ y \in V$
19	18 4	brcnv	$⊢ y R^{-1} x \leftrightarrow x R y$
20	19	notbii	$⊢ \neg y R^{-1} x \leftrightarrow \neg x R y$
21	20	ralbii	$⊢ \forall y \in B \neg y R^{-1} x \leftrightarrow \forall y \in B \neg x R y$
22		impexp	$⊢ ((y \in A \land \neg y \in R^{-1} [B]) \to \neg y R x) \leftrightarrow (y \in A \to (\neg y \in R^{-1} [B] \to \neg y R x))$
23		eldif	$⊢ y \in (A ∖ R^{-1} [B]) \leftrightarrow (y \in A \land \neg y \in R^{-1} [B])$
24	23	imbi1i	$⊢ (y \in (A ∖ R^{-1} [B]) \to \neg y R x) \leftrightarrow ((y \in A \land \neg y \in R^{-1} [B]) \to \neg y R x)$
25	18	elima	$⊢ y \in R^{-1} [B] \leftrightarrow \exists z \in B z R^{-1} y$
26		vex	$⊢ z \in V$
27	26 18	brcnv	$⊢ z R^{-1} y \leftrightarrow y R z$
28	27	rexbii	$⊢ \exists z \in B z R^{-1} y \leftrightarrow \exists z \in B y R z$
29	25 28	bitri	$⊢ y \in R^{-1} [B] \leftrightarrow \exists z \in B y R z$
30	29	imbi2i	$⊢ (y R x \to y \in R^{-1} [B]) \leftrightarrow (y R x \to \exists z \in B y R z)$
31		con34b	$⊢ (y R x \to y \in R^{-1} [B]) \leftrightarrow (\neg y \in R^{-1} [B] \to \neg y R x)$
32	30 31	bitr3i	$⊢ (y R x \to \exists z \in B y R z) \leftrightarrow (\neg y \in R^{-1} [B] \to \neg y R x)$
33	32	imbi2i	$⊢ (y \in A \to (y R x \to \exists z \in B y R z)) \leftrightarrow (y \in A \to (\neg y \in R^{-1} [B] \to \neg y R x))$
34	22 24 33	3bitr4i	$⊢ (y \in (A ∖ R^{-1} [B]) \to \neg y R x) \leftrightarrow (y \in A \to (y R x \to \exists z \in B y R z))$
35	34	ralbii2	$⊢ \forall y \in (A ∖ R^{-1} [B]) \neg y R x \leftrightarrow \forall y \in A (y R x \to \exists z \in B y R z)$
36	21 35	anbi12i	$⊢ (\forall y \in B \neg y R^{-1} x \land \forall y \in (A ∖ R^{-1} [B]) \neg y R x) \leftrightarrow (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$
37	6 17 36	3bitr2ri	$⊢ (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z)) \leftrightarrow x \in (V ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]]))$
38	3 37	mpgbir	$⊢ \{x \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} = V ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])$
39	38	ineq2i	$⊢ A \cap \{x \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} = A \cap (V ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]]))$
40		invdif	$⊢ A \cap (V ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])) = A ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])$
41	39 40	eqtri	$⊢ A \cap \{x \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} = A ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])$
42	2 41	eqtri	$⊢ \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} = A ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]])$
43	42	unieqi	$⊢ ⋃ \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} = ⋃ (A ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]]))$
44	1 43	eqtri	$⊢ sup (B, A, R) = ⋃ (A ∖ (R^{-1} [B] \cup R [A ∖ R^{-1} [B]]))$

Metamath Proof Explorer

Theorem dfsup2

Proof