Theorem th3q 3253

Description: Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs.

Hypotheses

Ref	Expression
th3q.1	|- R e. V
th3q.2	|- Er R
th3q.3	|- dom R = (S X. S)
th3q.4	|- ((((w e. S /\ v e. S) /\ (u e. S /\ t e. S)) /\ ((s e. S /\ f e. S) /\ (g e. S /\ h e. S))) -> ((<.w, v>.R<.u, t>. /\ <.s, f>.R<.g, h>.) -> (<.w, v>.F<.s, f>.)R(<.u, t>.F<.g, h>.)))
th3q.5	|- G = {<.<.x, y>., z>. | ((x e. ((S X. S)/.R) /\ y e. ((S X. S)/.R)) /\ E.wE.vE.uE.t((x = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R))}

Assertion

Ref	Expression
th3q	|- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> ([<.A, B>.]RG[<.C, D>.]R) = [(<.A, B>.F<.C, D>.)]R)

Distinct variable group(s):   x,y,z,w,v,u,t,s,f,g,h,R   x,S,y,z,w,v,u,t,s,f,g,h   x,A,y,z,w,v,u,t,s,f,g,h   x,B,y,z,w,v,u,t,s,f,g,h   x,C,y,z,w,v,u,t,s,f,g,h   x,D,y,z,w,v,u,t,s,f,g,h   x,F,y,z,w,v,u,t,s,f,g,h   x,G,y,z,w,v,u,t,s,f,g,h

Proof of Theorem th3q

Step	Hyp	Ref	Expression
1		th3q.1	. . . 4 |- R e. V
2		ecexg 3204	. . . 4 |- (R e. V -> [(<.A, B>.F<.C, D>.)]R e. V)
3	1, 2	ax-mp 6	. . 3 |- [(<.A, B>.F<.C, D>.)]R e. V
4		cleq1 1107	. . . . . 6 |- (x = [<.A, B>.]R -> (x = [<.w, v>.]R <-> [<.A, B>.]R = [<.w, v>.]R))
5	4	anbi1d 469	. . . . 5 |- (x = [<.A, B>.]R -> ((x = [<.w, v>.]R /\ y = [<.u, t>.]R) <-> ([<.A, B>.]R = [<.w, v>.]R /\ y = [<.u, t>.]R)))
6	5	anbi1d 469	. . . 4 |- (x = [<.A, B>.]R -> (((x = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R) <-> (([<.A, B>.]R = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R)))
7	6	bi4exdv 940	. . 3 |- (x = [<.A, B>.]R -> (E.wE.vE.uE.t((x = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R) <-> E.wE.vE.uE.t(([<.A, B>.]R = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R)))
8		cleq1 1107	. . . . . 6 |- (y = [<.C, D>.]R -> (y = [<.u, t>.]R <-> [<.C, D>.]R = [<.u, t>.]R))
9	8	anbi2d 468	. . . . 5 |- (y = [<.C, D>.]R -> (([<.A, B>.]R = [<.w, v>.]R /\ y = [<.u, t>.]R) <-> ([<.A, B>.]R = [<.w, v>.]R /\ [<.C, D>.]R = [<.u, t>.]R)))
10	9	anbi1d 469	. . . 4 |- (y = [<.C, D>.]R -> ((([<.A, B>.]R = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R) <-> (([<.A, B>.]R = [<.w, v>.]R /\ [<.C, D>.]R = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R)))
11	10	bi4exdv 940	. . 3 |- (y = [<.C, D>.]R -> (E.wE.vE.uE.t(([<.A, B>.]R = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R) <-> E.wE.vE.uE.t(([<.A, B>.]R = [<.w, v>.]R /\ [<.C, D>.]R = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R)))
12		cleq1 1107	. . . . 5 |- (z = [(<.A, B>.F<.C, D>.)]R -> (z = [(<.w, v>.F<.u, t>.)]R <-> [(<.A, B>.F<.C, D>.)]R = [(<.w, v>.F<.u, t>.)]R))
13	12	anbi2d 468	. . . 4 |- (z = [(<.A, B>.F<.C, D>.)]R -> ((([<.A, B>.]R = [<.w, v>.]R /\ [<.C, D>.]R = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R) <-> (([<.A, B>.]R = [<.w, v>.]R /\ [<.C, D>.]R = [<.u, t>.]R) /\ [(<.A, B>.F<.C, D>.)]R = [(<.w, v>.F<.u, t>.)]R)))
14	13	bi4exdv 940	. . 3 |- (z = [(<.A, B>.F<.C, D>.)]R -> (E.wE.vE.uE.t(([<.A, B>.]R = [<.w, v>.]R /\ [<.C, D>.]R = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R) <-> E.wE.vE.uE.t(([<.A, B>.]R = [<.w, v>.]R /\ [<.C, D>.]R = [<.u, t>.]R) /\ [(<.A, B>.F<.C, D>.)]R = [(<.w, v>.F<.u, t>.)]R)))
15		th3q.2	. . . 4 |- Er R
16		th3q.3	. . . 4 |- dom R = (S X. S)
17		th3q.4	. . . 4 |- ((((w e. S /\ v e. S) /\ (u e. S /\ t e. S)) /\ ((s e. S /\ f e. S) /\ (g e. S /\ h e. S))) -> ((<.w, v>.R<.u, t>. /\ <.s, f>.R<.g, h>.) -> (<.w, v>.F<.s, f>.)R(<.u, t>.F<.g, h>.)))
18	1, 15, 16, 17	th3qlem2 3251	. . 3 |- ((x e. ((S X. S)/.R) /\ y e. ((S X. S)/.R)) -> E*zE.wE.vE.uE.t((x = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R))
19		th3q.5	. . 3 |- G = {<.<.x, y>., z>. | ((x e. ((S X. S)/.R) /\ y e. ((S X. S)/.R)) /\ E.wE.vE.uE.t((x = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R))}
20	3, 7, 11, 14, 18, 19	oprabvali 3049	. 2 |- (([<.A, B>.]R e. ((S X. S)/.R) /\ [<.C, D>.]R e. ((S X. S)/.R)) -> (E.wE.vE.uE.t(([<.A, B>.]R = [<.w, v>.]R /\ [<.C, D>.]R = [<.u, t>.]R) /\ [(<.A, B>.F<.C, D>.)]R = [(<.w, v>.F<.u, t>.)]R) -> ([<.A, B>.]RG[<.C, D>.]R) = [(<.A, B>.F<.C, D>.)]R))
21		opelxpi 2455	. . . 4 |- ((A e. S /\ B e. S) -> <.A, B>. e. (S X. S))
22	1	ecelqsi 3229	. . . 4 |- (<.A, B>. e. (S X. S) -> [<.A, B>.]R e. ((S X. S)/.R))
23	21, 22	syl 12	. . 3 |- ((A e. S /\ B e. S) -> [<.A, B>.]R e. ((S X. S)/.R))
24		opelxpi 2455	. . . 4 |- ((C e. S /\ D e. S) -> <.C, D>. e. (S X. S))
25	1	ecelqsi 3229	. . . 4 |- (<.C, D>. e. (S X. S) -> [<.C, D>.]R