Theorem eropreu 15733

Description: Lemma for eroprv 15734 and eroprf 15735.

Hypotheses

Ref	Expression
eropr.1	|- J = (A/.R)
eropr.2	|- K = (B/.S)
eropr.3	|- (ph -> T e. Z)
eropr.4	|- (ph -> Er R)
eropr.5	|- (ph -> Er S)
eropr.6	|- (ph -> Er T)
eropr.7	|- (ph -> A C_ dom R)
eropr.8	|- (ph -> B C_ dom S)
eropr.9	|- (ph -> C C_ dom T)
eropr.10	|- (ph -> F:(A X. B)-->C)
eropr.11	|- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> ((rRs /\ tSu) -> (rFt)T(sFu)))

Assertion

Ref	Expression
eropreu	|- ((ph /\ (x e. J /\ y e. K)) -> E!zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))

Distinct variable groups:   A,p,q,r,s,t,u,x,z   B,p,q,r,s,t,u,y,z   R,p,q,r,s,t,u,x,z   S,p,q,r,s,t,u,y,z   T,p,q,r,s,t,u,z   F,p,q,r,s,t,u,z   ph,p,q,r,s,t,u,z   J,p,q,z   K,p,q,z

Proof of Theorem eropreu

Step	Hyp	Ref	Expression
1		eqeq1 1890	. . . . 5 |- (z = w -> (z = [(pFq)]T <-> w = [(pFq)]T))
2	1	anbi2d 678	. . . 4 |- (z = w -> (((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T)))
3	2	2rexbidv 2141	. . 3 |- (z = w -> (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T)))
4	3	eu4 1806	. 2 |- (E!zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> (E.zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) /\ A.zA.w((E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) /\ E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T)) -> z = w)))
5		eropr.1	. . . . . . . . . 10 |- J = (A/.R)
6	5	eleq2i 1961	. . . . . . . . 9 |- (x e. J <-> x e. (A/.R))
7		df-qs 5323	. . . . . . . . . 10 |- (A/.R) = {x | E.p e. A x = [p]R}
8	7	abeq2i 2001	. . . . . . . . 9 |- (x e. (A/.R) <-> E.p e. A x = [p]R)
9	6, 8	bitri 190	. . . . . . . 8 |- (x e. J <-> E.p e. A x = [p]R)
10		eropr.2	. . . . . . . . . 10 |- K = (B/.S)
11	10	eleq2i 1961	. . . . . . . . 9 |- (y e. K <-> y e. (B/.S))
12		df-qs 5323	. . . . . . . . . 10 |- (B/.S) = {y | E.q e. B y = [q]S}
13	12	abeq2i 2001	. . . . . . . . 9 |- (y e. (B/.S) <-> E.q e. B y = [q]S)
14	11, 13	bitri 190	. . . . . . . 8 |- (y e. K <-> E.q e. B y = [q]S)
15	9, 14	anbi12i 540	. . . . . . 7 |- ((x e. J /\ y e. K) <-> (E.p e. A x = [p]R /\ E.q e. B y = [q]S))
16	15	biimpi 168	. . . . . 6 |- ((x e. J /\ y e. K) -> (E.p e. A x = [p]R /\ E.q e. B y = [q]S))
17	16	adantl 424	. . . . 5 |- ((ph /\ (x e. J /\ y e. K)) -> (E.p e. A x = [p]R /\ E.q e. B y = [q]S))
18		reeanv 2249	. . . . 5 |- (E.p e. A E.q e. B (x = [p]R /\ y = [q]S) <-> (E.p e. A x = [p]R /\ E.q e. B y = [q]S))
19	17, 18	sylibr 217	. . . 4 |- ((ph /\ (x e. J /\ y e. K)) -> E.p e. A E.q e. B (x = [p]R /\ y = [q]S))
20		eropr.3	. . . . . . . 8 |- (ph -> T e. Z)
21	20	adantr 425	. . . . . . 7 |- ((ph /\ (x e. J /\ y e. K)) -> T e. Z)
22		ecexg 5322	. . . . . . 7 |- (T e. Z -> [(pFq)]T e. _V)
23		elex 2302	. . . . . . 7 |- ([(pFq)]T e. _V -> E.z z = [(pFq)]T)
24	21, 22, 23	3syl 24	. . . . . 6 |- ((ph /\ (x e. J /\ y e. K)) -> E.z z = [(pFq)]T)
25	24	biantrud 795	. . . . 5 |- ((ph /\ (x e. J /\ y e. K)) -> ((x = [p]R /\ y = [q]S) <-> ((x = [p]R /\ y = [q]S) /\ E.z z = [(pFq)]T)))
26	25	2rexbidv 2141	. . . 4 |- ((ph /\ (x e. J /\ y e. K)) -> (E.p e. A E.q e. B (x = [p]R /\ y = [q]S) <-> E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ E.z z = [(pFq)]T)))
27	19, 26	mpbid 212	. . 3 |- ((ph /\ (x e. J /\ y e. K)) -> E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ E.z z = [(pFq)]T))
28		19.42v 1688	. . . . . . . 8 |- (E.z((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> ((x = [p]R /\ y = [q]S) /\ E.z z = [(pFq)]T))
29	28	bicomi 189	. . . . . . 7 |- (((x = [p]R /\ y = [q]S) /\ E.z z = [(pFq)]T) <-> E.z((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))
30	29	rexbii 2128	. . . . . 6 |- (E.q e. B ((x = [p]R /\ y = [q]S) /\ E.z z = [(pFq)]T) <-> E.q e. B E.z((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))
31		rexcom4 2312	. . . . . 6 |- (E.q e. B E.z((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> E.zE.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))
32	30, 31	bitri 190	. . . . 5 |- (E.q e. B ((x = [p]R /\ y = [q]S) /\ E.z z = [(pFq)]T) <-> E.zE.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))
33	32	rexbii 2128	. . . 4 |- (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ E.z z = [(pFq)]T) <-> E.p e. A E.zE.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))
34		rexcom4 2312	. . . 4 |- (E.p e. A E.zE.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> E.zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))
35	33, 34	bitri 190	. . 3 |- (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ E.z z = [(pFq)]T) <-> E.zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))
36	27, 35	sylib 215	. 2 |- ((ph /\ (x e. J /\ y e. K)) -> E.zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))
37		eqeq12 1896	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z = [(rFt)]T /\ w = [(sFu)]T) -> (z = w <-> [(rFt)]T = [(sFu)]T))
38		eropr.11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> ((rRs /\ tSu) -> (rFt)T(sFu)))
39		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- s e. _V
40	39	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((ph /\ r e. A) -> s e. _V)
41		eropr.4	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (ph -> Er R)
42	41	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((ph /\ r e. A) -> Er R)
43		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((A C_ dom R /\ r e. A) -> r e. dom R)
44		eropr.7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (ph -> A C_ dom R)
45	43, 44	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((ph /\ r e. A) -> r e. dom R)
46		erthdmg 15730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((s e. _V /\ Er R /\ r e. dom R) -> ([r]R = [s]R <-> rRs))
47	40, 42, 45, 46	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((ph /\ r e. A) -> ([r]R = [s]R <-> rRs))
48	47	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((ph /\ (r e. A /\ t e. B)) -> ([r]R = [s]R <-> rRs))
49		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- u e. _V
50	49	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((ph /\ t e. B) -> u e. _V)
51		eropr.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (ph -> Er S)
52	51	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((ph /\ t e. B) -> Er S)
53		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((B C_ dom S /\ t e. B) -> t e. dom S)
54		eropr.8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (ph -> B C_ dom S)
55	53, 54	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((ph /\ t e. B) -> t e. dom S)
56		erthdmg 15730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((u e. _V /\ Er S /\ t e. dom S) -> ([t]S = [u]S <-> tSu))
57	50, 52, 55, 56	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((ph /\ t e. B) -> ([t]S = [u]S <-> tSu))
58	57	adantrl 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((ph /\ (r e. A /\ t e. B)) -> ([t]S = [u]S <-> tSu))
59	48, 58	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((ph /\ (r e. A /\ t e. B)) -> (([r]R = [s]R /\ [t]S = [u]S) <-> (rRs /\ tSu)))
60	59	adantrlr 437	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((ph /\ ((r e. A /\ s e. A) /\ t e. B)) -> (([r]R = [s]R /\ [t]S = [u]S) <-> (rRs /\ tSu)))
61	60	adantrrr 439	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> (([r]R = [s]R /\ [t]S = [u]S) <-> (rRs /\ tSu)))
62		foprrn 4965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F:(A X. B)-->C /\ r e. A /\ t e. B) -> (rFt) e. C)
63	62	3expb 1068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((F:(A X. B)-->C /\ (r e. A /\ t e. B)) -> (rFt) e. C)
64		eropr.10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (ph -> F:(A X. B)-->C)
65	63, 64	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((ph /\ (r e. A /\ t e. B)) -> (rFt) e. C)
66		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (sFu) e. _V
67	66	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((ph /\ (rFt) e. C) -> (sFu) e. _V)
68		eropr.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (ph -> Er T)
69	68	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((ph /\ (rFt) e. C) -> Er T)
70		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((C C_ dom T /\ (rFt) e. C) -> (rFt) e. dom T)
71		eropr.9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (ph -> C C_ dom T)
72	70, 71	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((ph /\ (rFt) e. C) -> (rFt) e. dom T)
73		erthdmg 15730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((sFu) e. _V /\ Er T /\ (rFt) e. dom T) -> ([(rFt)]T = [(sFu)]T <-> (rFt)T(sFu)))
74	67, 69, 72, 73	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((ph /\ (rFt) e. C) -> ([(rFt)]T = [(sFu)]T <-> (rFt)T(sFu)))
75	65, 74	syldan 516	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((ph /\ (r e. A /\ t e. B)) -> ([(rFt)]T = [(sFu)]T <-> (rFt)T(sFu)))
76	75	adantrlr 437	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((ph /\ ((r e. A /\ s e. A) /\ t e. B)) -> ([(rFt)]T = [(sFu)]T <-> (rFt)T(sFu)))
77	76	adantrrr 439	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> ([(rFt)]T = [(sFu)]T <-> (rFt)T(sFu)))
78	38, 61, 77	3imtr4d 602	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> (([r]R = [s]R /\ [t]S = [u]S) -> [(rFt)]T = [(sFu)]T))
79	78	imp 377	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) /\ ([r]R = [s]R /\ [t]S = [u]S)) -> [(rFt)]T = [(sFu)]T)
80		eqtr2 1905	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x = [r]R /\ x = [s]R) -> [r]R = [s]R)
81		eqtr2 1905	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y = [t]S /\ y = [u]S) -> [t]S = [u]S)
82	80, 81	anim12i 360	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((x = [r]R /\ x = [s]R) /\ (y = [t]S /\ y = [u]S)) -> ([r]R = [s]R /\ [t]S = [u]S))
83	82	an4s 566	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((x = [r]R /\ y = [t]S) /\ (x = [s]R /\ y = [u]S)) -> ([r]R = [s]R /\ [t]S = [u]S))
84	79, 83	sylan2 500	. . . . . . . . . . . . . . . . . . . . . 22 |- (((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) /\ ((x = [r]R /\ y = [t]S) /\ (x = [s]R /\ y = [u]S))) -> [(rFt)]T = [(sFu)]T)
85	37, 84	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . 21 |- (((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) /\ ((x = [r]R /\ y = [t]S) /\ (x = [s]R /\ y = [u]S))) -> ((z = [(rFt)]T /\ w = [(sFu)]T) -> z = w))
86	85	expcom 403	. . . . . . . . . . . . . . . . . . . 20 |- (((x = [r]R /\ y = [t]S) /\ (x = [s]R /\ y = [u]S)) -> ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> ((z = [(rFt)]T /\ w = [(sFu)]T) -> z = w)))
87	86	com23 36	. . . . . . . . . . . . . . . . . . 19 |- (((x = [r]R /\ y = [t]S) /\ (x = [s]R /\ y = [u]S)) -> ((z = [(rFt)]T /\ w = [(sFu)]T) -> ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> z = w)))
88	87	imp 377	. . . . . . . . . . . . . . . . . 18 |- ((((x = [r]R /\ y = [t]S) /\ (x = [s]R /\ y = [u]S)) /\ (z = [(rFt)]T /\ w = [(sFu)]T)) -> ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> z = w))
89	88	an4s 566	. . . . . . . . . . . . . . . . 17 |- ((((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) /\ ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T)) -> ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> z = w))
90	89	com12 14	. . . . . . . . . . . . . . . 16 |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> ((((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) /\ ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T)) -> z = w))
91	90	exp3a 405	. . . . . . . . . . . . . . 15 |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> (((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> (((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> z = w)))
92	91	expcom 403	. . . . . . . . . . . . . 14 |- (((r e. A /\ s e. A) /\ (t e. B /\ u e. B)) -> (ph -> (((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> (((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> z = w))))
93	92	an4s 566	. . . . . . . . . . . . 13 |- (((r e. A /\ t e. B) /\ (s e. A /\ u e. B)) -> (ph -> (((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> (((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> z = w))))
94	93	com12 14	. . . . . . . . . . . 12 |- (ph -> (((r e. A /\ t e. B) /\ (s e. A /\ u e. B)) -> (((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> (((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> z = w))))
95	94	expdimp 406	. . . . . . . . . . 11 |- ((ph /\ (r e. A /\ t e. B)) -> ((s e. A /\ u e. B) -> (((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> (((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> z = w))))
96	95	com34 40	. . . . . . . . . 10 |- ((ph /\ (r e. A /\ t e. B)) -> ((s e. A /\ u e. B) -> (((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> (((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> z = w))))
97	96	r19.23advv 2218	. . . . . . . . 9 |- ((ph /\ (r e. A /\ t e. B)) -> (E.s e. A E.u e. B ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> (((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> z = w)))
98	97	com23 36	. . . . . . . 8 |- ((ph /\ (r e. A /\ t e. B)) -> (((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> (E.s e. A E.u e. B ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> z = w)))
99	98	ex 402	. . . . . . 7 |- (ph -> ((r e. A /\ t e. B) -> (((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> (E.s e. A E.u e. B ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> z = w))))
100	99	r19.23advv 2218	. . . . . 6 |- (ph -> (E.r e. A E.t e. B ((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) -> (E.s e. A E.u e. B ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T) -> z = w)))
101	100	imp3a 388	. . . . 5 |- (ph -> ((E.r e. A E.t e. B ((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) /\ E.s e. A E.u e. B ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T)) -> z = w))
102		eceq2 5336	. . . . . . . . . . . 12 |- (p = r -> [p]R = [r]R)
103	102	eqeq2d 1895	. . . . . . . . . . 11 |- (p = r -> (x = [p]R <-> x = [r]R))
104	103	anbi1d 679	. . . . . . . . . 10 |- (p = r -> ((x = [p]R /\ y = [q]S) <-> (x = [r]R /\ y = [q]S)))
105		opreq1 4889	. . . . . . . . . . . 12 |- (p = r -> (pFq) = (rFq))
106		eceq2 5336	. . . . . . . . . . . 12 |- ((pFq) = (rFq) -> [(pFq)]T = [(rFq)]T)
107	105, 106	syl 12	. . . . . . . . . . 11 |- (p = r -> [(pFq)]T = [(rFq)]T)
108	107	eqeq2d 1895	. . . . . . . . . 10 |- (p = r -> (z = [(pFq)]T <-> z = [(rFq)]T))
109	104, 108	anbi12d 690	. . . . . . . . 9 |- (p = r -> (((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> ((x = [r]R /\ y = [q]S) /\ z = [(rFq)]T)))
110	109	rexbidv 2124	. . . . . . . 8 |- (p = r -> (E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> E.q e. B ((x = [r]R /\ y = [q]S) /\ z = [(rFq)]T)))
111	110	cbvrexv 2281	. . . . . . 7 |- (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> E.r e. A E.q e. B ((x = [r]R /\ y = [q]S) /\ z = [(rFq)]T))
112		eceq2 5336	. . . . . . . . . . . 12 |- (q = t -> [q]S = [t]S)
113	112	eqeq2d 1895	. . . . . . . . . . 11 |- (q = t -> (y = [q]S <-> y = [t]S))
114	113	anbi2d 678	. . . . . . . . . 10 |- (q = t -> ((x = [r]R /\ y = [q]S) <-> (x = [r]R /\ y = [t]S)))
115		opreq2 4890	. . . . . . . . . . . 12 |- (q = t -> (rFq) = (rFt))
116		eceq2 5336	. . . . . . . . . . . 12 |- ((rFq) = (rFt) -> [(rFq)]T = [(rFt)]T)
117	115, 116	syl 12	. . . . . . . . . . 11 |- (q = t -> [(rFq)]T = [(rFt)]T)
118	117	eqeq2d 1895	. . . . . . . . . 10 |- (q = t -> (z = [(rFq)]T <-> z = [(rFt)]T))
119	114, 118	anbi12d 690	. . . . . . . . 9 |- (q = t -> (((x = [r]R /\ y = [q]S) /\ z = [(rFq)]T) <-> ((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T)))
120	119	cbvrexv 2281	. . . . . . . 8 |- (E.q e. B ((x = [r]R /\ y = [q]S) /\ z = [(rFq)]T) <-> E.t e. B ((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T))
121	120	rexbii 2128	. . . . . . 7 |- (E.r e. A E.q e. B ((x = [r]R /\ y = [q]S) /\ z = [(rFq)]T) <-> E.r e. A E.t e. B ((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T))
122	111, 121	bitri 190	. . . . . 6 |- (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> E.r e. A E.t e. B ((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T))
123		eceq2 5336	. . . . . . . . . . . 12 |- (p = s -> [p]R = [s]R)
124	123	eqeq2d 1895	. . . . . . . . . . 11 |- (p = s -> (x = [p]R <-> x = [s]R))
125	124	anbi1d 679	. . . . . . . . . 10 |- (p = s -> ((x = [p]R /\ y = [q]S) <-> (x = [s]R /\ y = [q]S)))
126		opreq1 4889	. . . . . . . . . . . 12 |- (p = s -> (pFq) = (sFq))
127		eceq2 5336	. . . . . . . . . . . 12 |- ((pFq) = (sFq) -> [(pFq)]T = [(sFq)]T)
128	126, 127	syl 12	. . . . . . . . . . 11 |- (p = s -> [(pFq)]T = [(sFq)]T)
129	128	eqeq2d 1895	. . . . . . . . . 10 |- (p = s -> (w = [(pFq)]T <-> w = [(sFq)]T))
130	125, 129	anbi12d 690	. . . . . . . . 9 |- (p = s -> (((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T) <-> ((x = [s]R /\ y = [q]S) /\ w = [(sFq)]T)))
131	130	rexbidv 2124	. . . . . . . 8 |- (p = s -> (E.q e. B ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T) <-> E.q e. B ((x = [s]R /\ y = [q]S) /\ w = [(sFq)]T)))
132	131	cbvrexv 2281	. . . . . . 7 |- (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T) <-> E.s e. A E.q e. B ((x = [s]R /\ y = [q]S) /\ w = [(sFq)]T))
133		eceq2 5336	. . . . . . . . . . . 12 |- (q = u -> [q]S = [u]S)
134	133	eqeq2d 1895	. . . . . . . . . . 11 |- (q = u -> (y = [q]S <-> y = [u]S))
135	134	anbi2d 678	. . . . . . . . . 10 |- (q = u -> ((x = [s]R /\ y = [q]S) <-> (x = [s]R /\ y = [u]S)))
136		opreq2 4890	. . . . . . . . . . . 12 |- (q = u -> (sFq) = (sFu))
137		eceq2 5336	. . . . . . . . . . . 12 |- ((sFq) = (sFu) -> [(sFq)]T = [(sFu)]T)
138	136, 137	syl 12	. . . . . . . . . . 11 |- (q = u -> [(sFq)]T = [(sFu)]T)
139	138	eqeq2d 1895	. . . . . . . . . 10 |- (q = u -> (w = [(sFq)]T <-> w = [(sFu)]T))
140	135, 139	anbi12d 690	. . . . . . . . 9 |- (q = u -> (((x = [s]R /\ y = [q]S) /\ w = [(sFq)]T) <-> ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T)))
141	140	cbvrexv 2281	. . . . . . . 8 |- (E.q e. B ((x = [s]R /\ y = [q]S) /\ w = [(sFq)]T) <-> E.u e. B ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T))
142	141	rexbii 2128	. . . . . . 7 |- (E.s e. A E.q e. B ((x = [s]R /\ y = [q]S) /\ w = [(sFq)]T) <-> E.s e. A E.u e. B ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T))
143	132, 142	bitri 190	. . . . . 6 |- (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T) <-> E.s e. A E.u e. B ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T))
144	122, 143	anbi12i 540	. . . . 5 |- ((E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) /\ E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T)) <-> (E.r e. A E.t e. B ((x = [r]R /\ y = [t]S) /\ z = [(rFt)]T) /\ E.s e. A E.u e. B ((x = [s]R /\ y = [u]S) /\ w = [(sFu)]T)))
145	101, 144	syl5ib 223	. . . 4 |- (ph -> ((E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) /\ E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T)) -> z = w))
146	145	adantr 425	. . 3 |- ((ph /\ (x e. J /\ y e. K)) -> ((E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) /\ E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T)) -> z = w))
147	146	19.21aivv 1665	. 2 |- ((ph /\ (x e. J /\ y e. K)) -> A.zA.w((E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) /\ E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ w = [(pFq)]T)) -> z = w))
148	4, 36, 147	sylanbrc 527	1 |- ((ph /\ (x e. J /\ y e. K)) -> E!zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  E.wrex 2106  _Vcvv 2292   C_ wss 2593   class class class wbr 3338   X. cxp 3984  dom cdm 3986  -->wf 3994  (class class class)co 4884  Er wer 5315  [cec 5316  /.cqs 5317

This theorem is referenced by:  eroprv 15734  eroprf 15735

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-er 5318  df-ec 5320  df-qs 5323

Copyright terms: Public domain