Theorem brecop 4306

Description: Binary relation on a quotient set. Lemma for real number construction.

Hypotheses

Ref	Expression
brecop.1	|- S e. V
brecop.2	|- Er S
brecop.3	|- dom S = (G X. G)
brecop.4	|- H = ((G X. G)/.S)
brecop.5	|- R = {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))}
brecop.6	|- ((((z e. G /\ w e. G) /\ (A e. G /\ B e. G)) /\ ((v e. G /\ u e. G) /\ (C e. G /\ D e. G))) -> (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> (ph <-> ps)))

Assertion

Ref	Expression
brecop	|- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ([<.A, B>.]SR[<.C, D>.]S <-> ps))

Distinct variable groups:   x,y,z,w,v,u,A   x,B,y,z,w,v,u   x,C,y,z,w,v,u   x,D,y,z,w,v,u   x,S,y,z,w,v,u   x,H,y   z,G,w,v,u   ph,x,y   ps,z,w,v,u

Proof of Theorem brecop

Step	Hyp	Ref	Expression
1		eleq1 1534	. . . . . . . 8 |- (x = [<.A, B>.]S -> (x e. H <-> [<.A, B>.]S e. H))
2	1	anbi1d 617	. . . . . . 7 |- (x = [<.A, B>.]S -> ((x e. H /\ y e. H) <-> ([<.A, B>.]S e. H /\ y e. H)))
3		eqeq1 1481	. . . . . . . . . 10 |- (x = [<.A, B>.]S -> (x = [<.z, w>.]S <-> [<.A, B>.]S = [<.z, w>.]S))
4	3	anbi1d 617	. . . . . . . . 9 |- (x = [<.A, B>.]S -> ((x = [<.z, w>.]S /\ y = [<.v, u>.]S) <-> ([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S)))
5	4	anbi1d 617	. . . . . . . 8 |- (x = [<.A, B>.]S -> (((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph) <-> (([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph)))
6	5	4exbidv 1283	. . . . . . 7 |- (x = [<.A, B>.]S -> (E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph) <-> E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph)))
7	2, 6	anbi12d 628	. . . . . 6 |- (x = [<.A, B>.]S -> (((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph)) <-> (([<.A, B>.]S e. H /\ y e. H) /\ E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))))
8		eleq1 1534	. . . . . . . 8 |- (y = [<.C, D>.]S -> (y e. H <-> [<.C, D>.]S e. H))
9	8	anbi2d 616	. . . . . . 7 |- (y = [<.C, D>.]S -> (([<.A, B>.]S e. H /\ y e. H) <-> ([<.A, B>.]S e. H /\ [<.C, D>.]S e. H)))
10		eqeq1 1481	. . . . . . . . . 10 |- (y = [<.C, D>.]S -> (y = [<.v, u>.]S <-> [<.C, D>.]S = [<.v, u>.]S))
11	10	anbi2d 616	. . . . . . . . 9 |- (y = [<.C, D>.]S -> (([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) <-> ([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S)))
12	11	anbi1d 617	. . . . . . . 8 |- (y = [<.C, D>.]S -> ((([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph) <-> (([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph)))
13	12	4exbidv 1283	. . . . . . 7 |- (y = [<.C, D>.]S -> (E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph) <-> E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph)))
14	9, 13	anbi12d 628	. . . . . 6 |- (y = [<.C, D>.]S -> ((([<.A, B>.]S e. H /\ y e. H) /\ E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph)) <-> (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) /\ E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph))))
15	7, 14	opelopabg 2817	. . . . 5 |- (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) -> (<.[<.A, B>.]S, [<.C, D>.]S>. e. {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))} <-> (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) /\ E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph))))
16	15	bianabs 653	. . . 4 |- (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) -> (<.[<.A, B>.]S, [<.C, D>.]S>. e. {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))} <-> E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph)))
17		df-br 2620	. . . . 5 |- ([<.A, B>.]SR[<.C, D>.]S <-> <.[<.A, B>.]S, [<.C, D>.]S>. e. R)
18		brecop.5	. . . . . 6 |- R = {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))}
19	18	eleq2i 1538	. . . . 5 |- (<.[<.A, B>.]S, [<.C, D>.]S>. e. R <-> <.[<.A, B>.]S, [<.C, D>.]S>. e. {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))})
20	17, 19	bitr 173	. . . 4 |- ([<.A, B>.]SR[<.C, D>.]S <-> <.[<.A, B>.]S, [<.C, D>.]S>. e. {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))})
21	16, 20	syl5bb 532	. . 3 |- (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) -> ([<.A, B>.]SR[<.C, D>.]S <-> E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph)))
22		brecop.1	. . . 4 |- S e. V
23		brecop.4	. . . 4 |- H = ((G X. G)/.S)
24	22, 23	ecopqsi 4293	. . 3 |- ((A e. G /\ B e. G) -> [<.A, B>.]S e. H)
25	22, 23	ecopqsi 4293	. . 3 |- ((C e. G /\ D e. G) -> [<.C, D>.]S e. H)
26	21, 24, 25	syl2an 454	. 2 |-