Theorem brecop 3242

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 group(s):   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 1149	. . . . . . . 8 |- (x = [<.A, B>.]S -> (x e. H <-> [<.A, B>.]S e. H))
2	1	anbi1d 469	. . . . . . 7 |- (x = [<.A, B>.]S -> ((x e. H /\ y e. H) <-> ([<.A, B>.]S e. H /\ y e. H)))
3		cleq1 1107	. . . . . . . . . 10 |- (x = [<.A, B>.]S -> (x = [<.z, w>.]S <-> [<.A, B>.]S = [<.z, w>.]S))
4	3	anbi1d 469	. . . . . . . . 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 469	. . . . . . . 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	bi4exdv 940	. . . . . . 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 476	. . . . . 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 1149	. . . . . . . 8 |- (y = [<.C, D>.]S -> (y e. H <-> [<.C, D>.]S e. H))
9	8	anbi2d 468	. . . . . . 7 |- (y = [<.C, D>.]S -> (([<.A, B>.]S e. H /\ y e. H) <-> ([<.A, B>.]S e. H /\ [<.C, D>.]S e. H)))
10		cleq1 1107	. . . . . . . . . 10 |- (y = [<.C, D>.]S -> (y = [<.v, u>.]S <-> [<.C, D>.]S = [<.v, u>.]S))
11	10	anbi2d 468	. . . . . . . . 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 469	. . . . . . . 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	bi4exdv 940	. . . . . . 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 476	. . . . . 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 2115	. . . . 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		ibar 487	. . . . 5 |- (([<.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) <-> (([<.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))))
17	15, 16	bitr4d 409	. . . 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)))
18		df-br 2063	. . . . 5 |- ([<.A, B>.]SR[<.C, D>.]S <-> <.[<.A, B>.]S, [<.C, D>.]S>. e. R)
19		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))}
20	19	eleq2i 1153	. . . . 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))})
21	18, 20	bitr 151	. . . 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))})
22	17, 21	syl5bb 410	. . 3 |- (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) -> ([<.A, B>.]SR[<.C, D>.]S