Theorem dfsup2

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

	Ref	Expression
Assertion	dfsup2	$$⊢sup\left(B,A,R\right)=\bigcup \left(A\setminus \left(R^{-1}\left[B\right]\cup R\left[A\setminus R^{-1}\left[B\right]\right]\right)\right)$$

Proof

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