Theorem oprec 4318

Description: Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. (See set.mm for additional comments for the hypotheses.)

Hypotheses

Ref	Expression
oprec.1	|- H e. V
oprec.2	|- K e. V
oprec.3	|- L e. V
oprec.4	|- R e. V
oprec.5	|- Er R
oprec.6	|- dom R = (S X. S)
oprec.7	|- R = {<.x, y>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ ph))}
oprec.8	|- (((z = a /\ w = b) /\ (v = c /\ u = d)) -> (ph <-> ps))
oprec.9	|- (((z = g /\ w = h) /\ (v = t /\ u = s)) -> (ph <-> ch))
oprec.10	|- G = {<.<.x, y>., z>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = J))}
oprec.11	|- (((w = a /\ v = b) /\ (u = g /\ f = h)) -> J = K)
oprec.12	|- (((w = c /\ v = d) /\ (u = t /\ f = s)) -> J = L)
oprec.13	|- (((w = A /\ v = B) /\ (u = C /\ f = D)) -> J = H)
oprec.14	|- F = {<.<.x, y>., z>. | ((x e. Q /\ y e. Q) /\ E.aE.bE.cE.d((x = [<.a, b>.]R /\ y = [<.c, d>.]R) /\ z = [(<.a, b>.G<.c, d>.)]R))}
oprec.15	|- Q = ((S X. S)/.R)
oprec.16	|- ((((a e. S /\ b e. S) /\ (c e. S /\ d e. S)) /\ ((g e. S /\ h e. S) /\ (t e. S /\ s e. S))) -> ((ps /\ ch) -> KRL))

Assertion

Ref	Expression
oprec	|- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> ([<.A, B>.]RF[<.C, D>.]R) = [H]R)

Distinct variable groups:   x,y,z,w,v,u,t,s,f,g,h,a,b,c,d,A   x,B,y,z,w,v,u,t,s,f,g,h,a,b,c,d   x,C,y,z,w,v,u,t,s,f,g,h,a,b,c,d   x,D,y,z,w,v,u,t,s,f,g,h,a,b,c,d   x,F,y,z,t,s,g,h,a,b,c,d   x,G,y,z,t,s,g,h,a,b,c,d   x,H,y,z,w,v,u,f   x,J,y,z   x,K,y,z,w,v,u,f   x,L,y,z,w,v,u,f   x,Q,y,z,a,b,c,d   x,R,y,z,t,s,g,h,a,b,c,d   x,S,y,z,w,v,u,t,s,f,g,h,a,b,c,d   ph,x,y   ps,z,w,v,u   ch,z,w,v,u

Proof of Theorem oprec

Step	Hyp	Ref	Expression
1		oprec.4	. . 3 |- R e. V
2		oprec.5	. . 3 |- Er R
3		oprec.6	. . 3 |- dom R = (S X. S)
4		oprec.16	. . . 4 |- ((((a e. S /\ b e. S) /\ (c e. S /\ d e. S)) /\ ((g e. S /\ h e. S) /\ (t e. S /\ s e. S))) -> ((ps /\ ch) -> KRL))
5		oprec.8	. . . . . 6 |- (((z = a /\ w = b) /\ (v = c /\ u = d)) -> (ph <-> ps))
6		oprec.7	. . . . . 6 |- R = {<.x, y>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ ph))}
7	5, 6	opbrop 3238	. . . . 5 |- (((a e. S /\ b e. S) /\ (c e. S /\ d e. S)) -> (<.a, b>.R<.c, d>. <-> ps))
8		oprec.9	. . . . . 6 |- (((z = g /\ w = h) /\ (v = t /\ u = s)) -> (ph <-> ch))
9	8, 6	opbrop 3238	. . . . 5 |- (((g e. S /\ h e. S) /\ (t e. S /\ s e. S)) -> (<.g, h>.R<.t, s>. <-> ch))
10	7, 9	bi2anan9 632	. . . 4 |- ((((a e. S /\ b e. S) /\ (c e. S /\ d e. S)) /\ ((g e. S /\ h e. S) /\ (t e. S /\ s e. S))) -> ((<.a, b>.R<.c, d>. /\ <.g, h>.R<.t, s>.) <-> (ps /\ ch)))
11		oprec.2	. . . . . . 7 |- K e. V
12		oprec.11	. . . . . . 7 |- (((w = a /\ v = b) /\ (u = g /\ f = h)) -> J = K)
13		oprec.10	. . . . . . 7 |- G = {<.<.x, y>., z>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = J))}
14	11, 12, 13	oprabval3 4030	. . . . . 6 |- (((a e. S /\ b e. S) /\ (g e. S /\ h e. S)) -> (<.a, b>.G<.g, h>.) = K)
15		oprec.3	. . . . . . 7 |- L e. V
16		oprec.12	. . . . . . 7 |- (((w = c /\ v = d) /\ (u = t /\ f = s)) -> J = L)
17	15, 16, 13	oprabval3 4030	. . . . . 6 |- (((c e. S /\ d e. S) /\ (t e. S /\ s e. S)) -> (<.c, d>.G<.t, s>.) = L)
18	14, 17	breqan12d 2632	. . . . 5 |- ((((a e. S /\ b e. S) /\ (g e. S /\ h e. S)) /\ ((c e. S /\ d e. S) /\ (t e. S /\ s e. S))) -> ((<.a, b>.G<.g, h>.)R(<.c, d>.G<.t, s>.) <-> KRL))
19	18	an4s 508	. . . 4 |- ((((a e. S /\ b e. S) /\ (c e. S /\ d e. S)) /\ ((g e. S /\ h e. S) /\ (t e. S /\ s e. S))) -> ((<.a, b>.G<.g, h>.)R(<.c, d>.G<.t, s>.) <-> KRL))
20	4, 10, 19	3imtr4d 543	. . 3 |- ((((a e. S /\ b e. S) /\ (c e. S /\ d e. S)) /\ ((g e. S /\ h e. S) /\ (t e. S /\ s e. S))) -> ((<.a, b>.R<.c, d>. /\ <.g, h>.R<.t, s>.) -> (<.a, b>.G<.g, h>.)R(<.c, d>.G<.t, s>.)))
21		oprec.14	. . . 4 |- F = {<.<.x, y>., z>. | ((x e. Q /\ y e. Q) /\ E.aE.bE.cE.d((x = [<.a, b>.]R /\ y = [<.c, d>.]R) /\ z = [(<.a, b>.G<.c, d>.)]R))}
22		oprec.15	. . . . . . . 8 |- Q = ((S X. S)/.R)
23	22	eleq2i 1538	. . . . . . 7 |- (x e. Q <-> x e. ((S X. S)/.R))
24	22	eleq2i 1538	. . . . . . 7 |- (y e. Q <-> y e. ((S X. S)/.R))
25	23, 24	anbi12i 482	. . . . . 6 |- ((x e. Q /\ y e. Q) <-> (x e. ((S X. S)/.R) /\ y e. ((S X. S)/.R)))
26	25	anbi1i 481	. . . . 5 |- (((x e. Q /\ y e. Q) /\ E.aE.bE.cE.d((x = [<.a, b>.]R /\ y = [<.c, d>.]R) /\ z = [(<.a, b>.G<.c, d>.)]R)) <-> ((x e. ((S X. S)/.R) /\ y e. ((S X. S)/.R)) /\ E.aE.bE.cE.d((x = [<.a, b>.]R /\ y = [<.c, d>.]R) /\ z = [(<.a, b>.G<.c, d>.)]R)))
27	26	oprabbii 3997	. . . 4 |- {<.<.x, y>., z>. | ((x e. Q /\ y e. Q) /\ E.aE.bE.cE.d((x = [<.a, b>.]R /\ y = [<.c, d>.]R) /\ z = [(<.a, b>.G<.c, d>.)]R))} = {<.<.x, y>., z>. | ((x e. ((S X. S)/.R) /\ y e. ((S X. S)/.R)) /\ E.aE.bE.cE.d((x = [<.a, b>.]R /\ y = [<.c, d>.]R) /\ z = [(<.a, b>.G<.c, d>.)]R))}
28	21, 27	eqtr 1495	. . 3 |- F = {<.<.x, y>., z>. | ((x e. ((S X. S)/.R) /\ y e. ((S X. S)/.R)) /\ E.aE.bE.cE.d((x = [<.a, b>.]R /\ y = [<.c, d>.]R) /\ z = [(<.a, b>.G<.c, d>.)]R))}
29	1, 2, 3, 20, 28	th3q 4317	. 2 |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> ([<.A, B>.]RF[<.C, D>.]R) = [(<.A, B>.G<.C, D>.)]R)
30		oprec.1	. . . 4 |- H e. V
31		oprec.13	. . . 4 |- (((w = A /\