Theorem th3qlem2 4305

Description: Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption.

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>.)))

Assertion

Ref	Expression
th3qlem2	|- ((A e. ((S X. S)/.R) /\ B e. ((S X. S)/.R)) -> E*zE.wE.vE.uE.t((A = [<.w, v>.]R /\ B = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R))

Distinct variable groups:   z,w,v,u,t,s,f,g,h,R   z,S,w,v,u,t,s,f,g,h   z,A,w,v,u,t,s,f,g,h   z,B,w,v,u,t,s,f,g,h   z,F,w,v,u,t,s,f,g,h

Proof of Theorem th3qlem2

Step	Hyp	Ref	Expression
1		th3q.2	. . 3 |- Er R
2		th3q.3	. . 3 |- dom R = (S X. S)
3		eqid 1473	. . . . 5 |- (S X. S) = (S X. S)
4		breq1 2617	. . . . . . . 8 |- (<.w, v>. = s -> (<.w, v>.R<.u, t>. <-> sR<.u, t>.))
5	4	anbi1d 616	. . . . . . 7 |- (<.w, v>. = s -> ((<.w, v>.R<.u, t>. /\ xRy) <-> (sR<.u, t>. /\ xRy)))
6		opreq1 3959	. . . . . . . 8 |- (<.w, v>. = s -> (<.w, v>.Fx) = (sFx))
7	6	breq1d 2624	. . . . . . 7 |- (<.w, v>. = s -> ((<.w, v>.Fx)R(<.u, t>.Fy) <-> (sFx)R(<.u, t>.Fy)))
8	5, 7	imbi12d 625	. . . . . 6 |- (<.w, v>. = s -> (((<.w, v>.R<.u, t>. /\ xRy) -> (<.w, v>.Fx)R(<.u, t>.Fy)) <-> ((sR<.u, t>. /\ xRy) -> (sFx)R(<.u, t>.Fy))))
9	8	imbi2d 611	. . . . 5 |- (<.w, v>. = s -> (((x e. (S X. S) /\ y e. (S X. S)) -> ((<.w, v>.R<.u, t>. /\ xRy) -> (<.w, v>.Fx)R(<.u, t>.Fy))) <-> ((x e. (S X. S) /\ y e. (S X. S)) -> ((sR<.u, t>. /\ xRy) -> (sFx)R(<.u, t>.Fy)))))
10		breq2 2618	. . . . . . . 8 |- (<.u, t>. = f -> (sR<.u, t>. <-> sRf))
11	10	anbi1d 616	. . . . . . 7 |- (<.u, t>. = f -> ((sR<.u, t>. /\ xRy) <-> (sRf /\ xRy)))
12		opreq1 3959	. . . . . . . 8 |- (<.u, t>. = f -> (<.u, t>.Fy) = (fFy))
13	12	breq2d 2625	. . . . . . 7 |- (<.u, t>. = f -> ((sFx)R(<.u, t>.Fy) <-> (sFx)R(fFy)))
14	11, 13	imbi12d 625	. . . . . 6 |- (<.u, t>. = f -> (((sR<.u, t>. /\ xRy) -> (sFx)R(<.u, t>.Fy)) <-> ((sRf /\ xRy) -> (sFx)R(fFy))))
15	14	imbi2d 611	. . . . 5 |- (<.u, t>. = f -> (((x e. (S X. S) /\ y e. (S X. S)) -> ((sR<.u, t>. /\ xRy) -> (sFx)R(<.u, t>.Fy))) <-> ((x e. (S X. S) /\ y e. (S X. S)) -> ((sRf /\ xRy) -> (sFx)R(fFy)))))
16		breq1 2617	. . . . . . . . . 10 |- (<.s, f>. = x -> (<.s, f>.R<.g, h>. <-> xR<.g, h>.))
17	16	anbi2d 615	. . . . . . . . 9 |- (<.s, f>. = x -> ((<.w, v>.R<.u, t>. /\ <.s, f>.R<.g, h>.) <-> (<.w, v>.R<.u, t>. /\ xR<.g, h>.)))
18		opreq2 3960	. . . . . . . . . 10 |- (<.s, f>. = x -> (<.w, v>.F<.s, f>.) = (<.w, v>.Fx))
19	18	breq1d 2624	. . . . . . . . 9 |- (<.s, f>. = x -> ((<.w, v>.F<.s, f>.)R(<.u, t>.F<.g, h>.) <-> (<.w, v>.Fx)R(<.u, t>.F<.g, h>.)))
20	17, 19	imbi12d 625	. . . . . . . 8 |- (<.s, f>. = x -> (((<.w, v>.R<.u, t>. /\ <.s, f>.R<.g, h>.) -> (<.w, v>.F<.s, f>.)R(<.u, t>.F<.g, h>.)) <-> ((<.w, v>.R<.u, t>. /\ xR<.g, h>.) -> (<.w, v>.Fx)R(<.u, t>.F<.g, h>.))))
21	20	imbi2d 611	. . . . . . 7 |- (<.s, f>. = x -> ((((w e. S /\ v e. S) /\ (u e. S /\ t e. S)) -> ((<.w, v>.R<.u, t>. /\ <.s, f>.R<.g, h>.) -> (<.w, v>.F<.s, f>.)R(<.u, t>.F<.g, h>.))) <-> (((w e. S /\ v e. S) /\ (u e. S /\ t e. S)) -> ((<.w, v>.R<.u, t>. /\ xR<.g, h>.) -> (<.w, v>.Fx)R(<.u, t>.F<.g, h>.)))))
22		breq2 2618	. . . . . . . . . 10 |- (<.g, h>. = y -> (xR<.g, h>. <-> xRy))
23	22	anbi2d 615	. . . . . . . . 9 |- (<.g, h>. = y -> ((<.w, v>.R<.u, t>. /\ xR<.g, h>.) <-> (<.w, v>.R<.u, t>. /\ xRy)))
24		opreq2 3960	. . . . . . . . . 10 |- (<.g, h>. = y -> (<.u, t>.F<.g, h>.) = (<.u, t>.Fy))
25	24	breq2d 2625	. . . . . . . . 9 |- (<.g, h>. = y -> ((<.w, v>.Fx)R(<.u, t>.F<.g, h>.) <-> (<.w, v>.Fx)R(<.u, t>.Fy)))
26	23, 25	imbi12d 625	. . . . . . . 8 |- (<.g, h>. = y -> (((<.w, v>.R<.u, t>. /\ xR<.g, h>.) -> (<.w, v>.Fx)R(<.u, t>.F<.g, h>.)) <-> ((<.w, v>.R<.u, t>. /\ xRy) -> (<.w, v>.Fx)R(<.u, t>.Fy))))
27	26	imbi2d 611	. . . . . . 7 |- (<.g, h>. = y -> ((((w e. S /\ v e. S) /\ (u e. S /\ t e. S)) -> ((<.w, v>.R<.u, t>. /\ xR<.g, h>.) -> (<.w, v>.Fx)R(<.u, t>.F<.g, h>.))) <-> (((w e. S /\ v e. S) /\ (u e. S /\ t e. S)) -> ((<.w, v>.R<.u, t>. /\ xRy) -> (<.w, v>.Fx)R(<.u, t>.Fy)))))
28		th3q.4	. . . . . . . 8 |- ((((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>.)))
29	28	expcom 374	. . . . . . 7 |- (((s e. S /\ f e. S) /\ (g e. S /\ h e. S)) -> (((w e. S /\ v e. S) /\ (u e. S /\ t e. S)) -> ((<.w, v>.R<.u, t>. /\ <.s, f>.R<.g, h>.) -> (<.w, v>.F<.s, f>.)R(<.u, t>.F<.g, h>.))))
30	3, 21, 27, 29	2optocl 3231	. . . . . 6 |- ((x e. (S X. S) /\ y e. (S X. S)) -> (((w e. S /\ v e. S) /\ (u e. S /\ t e. S)) -> ((<.w, v>.R<.u, t>. /\ xRy) -> (<.w, v>.Fx)R(<.u, t>.Fy))))
31	30	com12 11	. . . . 5 |- (((w e. S /\