Metamath Proof Explorer

Theorem eroveu

Description: Lemma for erov and eroprf . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 9-Jul-2014)

Ref Expression
Hypotheses eropr.1 
|- J = ( A /. R )
eropr.2 
|- K = ( B /. S )
eropr.3 
|- ( ph -> T e. Z )
eropr.4 
|- ( ph -> R Er U )
eropr.5 
|- ( ph -> S Er V )
eropr.6 
|- ( ph -> T Er W )
eropr.7 
|- ( ph -> A C_ U )
eropr.8 
|- ( ph -> B C_ V )
eropr.9 
|- ( ph -> C C_ W )
eropr.10 
|- ( ph -> .+ : ( A X. B ) --> C )
eropr.11 
|- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )
Assertion eroveu 
|- ( ( ph /\ ( X e. J /\ Y e. K ) ) -> E! z E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )

Proof

Step Hyp Ref Expression
1 eropr.1 
 |-  J = ( A /. R )
2 eropr.2 
 |-  K = ( B /. S )
3 eropr.3 
 |-  ( ph -> T e. Z )
4 eropr.4 
 |-  ( ph -> R Er U )
5 eropr.5 
 |-  ( ph -> S Er V )
6 eropr.6 
 |-  ( ph -> T Er W )
7 eropr.7 
 |-  ( ph -> A C_ U )
8 eropr.8 
 |-  ( ph -> B C_ V )
9 eropr.9 
 |-  ( ph -> C C_ W )
10 eropr.10 
 |-  ( ph -> .+ : ( A X. B ) --> C )
11 eropr.11 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )
12 elqsi 
 |-  ( X e. ( A /. R ) -> E. p e. A X = [ p ] R )
13 12 1 eleq2s 
 |-  ( X e. J -> E. p e. A X = [ p ] R )
14 elqsi 
 |-  ( Y e. ( B /. S ) -> E. q e. B Y = [ q ] S )
15 14 2 eleq2s 
 |-  ( Y e. K -> E. q e. B Y = [ q ] S )
16 13 15 anim12i 
 |-  ( ( X e. J /\ Y e. K ) -> ( E. p e. A X = [ p ] R /\ E. q e. B Y = [ q ] S ) )
17 16 adantl 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> ( E. p e. A X = [ p ] R /\ E. q e. B Y = [ q ] S ) )
18 reeanv 
 |-  ( 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 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> E. p e. A E. q e. B ( X = [ p ] R /\ Y = [ q ] S ) )
20 3 adantr 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> T e. Z )
21 ecexg 
 |-  ( T e. Z -> [ ( p .+ q ) ] T e. _V )
22 elisset 
 |-  ( [ ( p .+ q ) ] T e. _V -> E. z z = [ ( p .+ q ) ] T )
23 20 21 22 3syl 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> E. z z = [ ( p .+ q ) ] T )
24 23 biantrud 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> ( ( X = [ p ] R /\ Y = [ q ] S ) <-> ( ( X = [ p ] R /\ Y = [ q ] S ) /\ E. z z = [ ( p .+ q ) ] T ) ) )
25 24 2rexbidv 
 |-  ( ( 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 = [ ( p .+ q ) ] T ) ) )
26 19 25 mpbid 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ E. z z = [ ( p .+ q ) ] T ) )
27 19.42v 
 |-  ( E. z ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> ( ( X = [ p ] R /\ Y = [ q ] S ) /\ E. z z = [ ( p .+ q ) ] T ) )
28 27 bicomi 
 |-  ( ( ( X = [ p ] R /\ Y = [ q ] S ) /\ E. z z = [ ( p .+ q ) ] T ) <-> E. z ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
29 28 rexbii 
 |-  ( E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ E. z z = [ ( p .+ q ) ] T ) <-> E. q e. B E. z ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
30 rexcom4 
 |-  ( E. q e. B E. z ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> E. z E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
31 29 30 bitri 
 |-  ( E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ E. z z = [ ( p .+ q ) ] T ) <-> E. z E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
32 31 rexbii 
 |-  ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ E. z z = [ ( p .+ q ) ] T ) <-> E. p e. A E. z E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
33 rexcom4 
 |-  ( E. p e. A E. z E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> E. z E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
34 32 33 bitri 
 |-  ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ E. z z = [ ( p .+ q ) ] T ) <-> E. z E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
35 26 34 sylib 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> E. z E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
36 reeanv 
 |-  ( E. r e. A E. s e. A ( E. t e. B ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ E. u e. B ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) <-> ( E. r e. A E. t e. B ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ E. s e. A E. u e. B ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) )
37 eceq1 
 |-  ( p = r -> [ p ] R = [ r ] R )
38 37 eqeq2d 
 |-  ( p = r -> ( X = [ p ] R <-> X = [ r ] R ) )
39 38 anbi1d 
 |-  ( p = r -> ( ( X = [ p ] R /\ Y = [ q ] S ) <-> ( X = [ r ] R /\ Y = [ q ] S ) ) )
40 oveq1 
 |-  ( p = r -> ( p .+ q ) = ( r .+ q ) )
41 40 eceq1d 
 |-  ( p = r -> [ ( p .+ q ) ] T = [ ( r .+ q ) ] T )
42 41 eqeq2d 
 |-  ( p = r -> ( z = [ ( p .+ q ) ] T <-> z = [ ( r .+ q ) ] T ) )
43 39 42 anbi12d 
 |-  ( p = r -> ( ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> ( ( X = [ r ] R /\ Y = [ q ] S ) /\ z = [ ( r .+ q ) ] T ) ) )
44 eceq1 
 |-  ( q = t -> [ q ] S = [ t ] S )
45 44 eqeq2d 
 |-  ( q = t -> ( Y = [ q ] S <-> Y = [ t ] S ) )
46 45 anbi2d 
 |-  ( q = t -> ( ( X = [ r ] R /\ Y = [ q ] S ) <-> ( X = [ r ] R /\ Y = [ t ] S ) ) )
47 oveq2 
 |-  ( q = t -> ( r .+ q ) = ( r .+ t ) )
48 47 eceq1d 
 |-  ( q = t -> [ ( r .+ q ) ] T = [ ( r .+ t ) ] T )
49 48 eqeq2d 
 |-  ( q = t -> ( z = [ ( r .+ q ) ] T <-> z = [ ( r .+ t ) ] T ) )
50 46 49 anbi12d 
 |-  ( q = t -> ( ( ( X = [ r ] R /\ Y = [ q ] S ) /\ z = [ ( r .+ q ) ] T ) <-> ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) ) )
51 43 50 cbvrex2vw 
 |-  ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> E. r e. A E. t e. B ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) )
52 eceq1 
 |-  ( p = s -> [ p ] R = [ s ] R )
53 52 eqeq2d 
 |-  ( p = s -> ( X = [ p ] R <-> X = [ s ] R ) )
54 53 anbi1d 
 |-  ( p = s -> ( ( X = [ p ] R /\ Y = [ q ] S ) <-> ( X = [ s ] R /\ Y = [ q ] S ) ) )
55 oveq1 
 |-  ( p = s -> ( p .+ q ) = ( s .+ q ) )
56 55 eceq1d 
 |-  ( p = s -> [ ( p .+ q ) ] T = [ ( s .+ q ) ] T )
57 56 eqeq2d 
 |-  ( p = s -> ( w = [ ( p .+ q ) ] T <-> w = [ ( s .+ q ) ] T ) )
58 54 57 anbi12d 
 |-  ( p = s -> ( ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) <-> ( ( X = [ s ] R /\ Y = [ q ] S ) /\ w = [ ( s .+ q ) ] T ) ) )
59 eceq1 
 |-  ( q = u -> [ q ] S = [ u ] S )
60 59 eqeq2d 
 |-  ( q = u -> ( Y = [ q ] S <-> Y = [ u ] S ) )
61 60 anbi2d 
 |-  ( q = u -> ( ( X = [ s ] R /\ Y = [ q ] S ) <-> ( X = [ s ] R /\ Y = [ u ] S ) ) )
62 oveq2 
 |-  ( q = u -> ( s .+ q ) = ( s .+ u ) )
63 62 eceq1d 
 |-  ( q = u -> [ ( s .+ q ) ] T = [ ( s .+ u ) ] T )
64 63 eqeq2d 
 |-  ( q = u -> ( w = [ ( s .+ q ) ] T <-> w = [ ( s .+ u ) ] T ) )
65 61 64 anbi12d 
 |-  ( q = u -> ( ( ( X = [ s ] R /\ Y = [ q ] S ) /\ w = [ ( s .+ q ) ] T ) <-> ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) )
66 58 65 cbvrex2vw 
 |-  ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) <-> E. s e. A E. u e. B ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) )
67 51 66 anbi12i 
 |-  ( ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) /\ E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) ) <-> ( E. r e. A E. t e. B ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ E. s e. A E. u e. B ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) )
68 36 67 bitr4i 
 |-  ( E. r e. A E. s e. A ( E. t e. B ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ E. u e. B ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) <-> ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) /\ E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) ) )
69 reeanv 
 |-  ( E. t e. B E. u e. B ( ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) <-> ( E. t e. B ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ E. u e. B ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) )
70 4 adantr 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> R Er U )
71 7 adantr 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> A C_ U )
72 simprll 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> r e. A )
73 71 72 sseldd 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> r e. U )
74 70 73 erth 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( r R s <-> [ r ] R = [ s ] R ) )
75 5 adantr 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> S Er V )
76 8 adantr 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> B C_ V )
77 simprrl 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> t e. B )
78 76 77 sseldd 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> t e. V )
79 75 78 erth 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( t S u <-> [ t ] S = [ u ] S ) )
80 74 79 anbi12d 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) <-> ( [ r ] R = [ s ] R /\ [ t ] S = [ u ] S ) ) )
81 6 adantr 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> T Er W )
82 9 adantr 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> C C_ W )
83 10 adantr 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> .+ : ( A X. B ) --> C )
84 83 72 77 fovrnd 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( r .+ t ) e. C )
85 82 84 sseldd 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( r .+ t ) e. W )
86 81 85 erth 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r .+ t ) T ( s .+ u ) <-> [ ( r .+ t ) ] T = [ ( s .+ u ) ] T ) )
87 11 80 86 3imtr3d 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( [ r ] R = [ s ] R /\ [ t ] S = [ u ] S ) -> [ ( r .+ t ) ] T = [ ( s .+ u ) ] T ) )
88 eqeq2 
 |-  ( w = [ ( s .+ u ) ] T -> ( [ ( r .+ t ) ] T = w <-> [ ( r .+ t ) ] T = [ ( s .+ u ) ] T ) )
89 88 biimprcd 
 |-  ( [ ( r .+ t ) ] T = [ ( s .+ u ) ] T -> ( w = [ ( s .+ u ) ] T -> [ ( r .+ t ) ] T = w ) )
90 87 89 syl6 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( [ r ] R = [ s ] R /\ [ t ] S = [ u ] S ) -> ( w = [ ( s .+ u ) ] T -> [ ( r .+ t ) ] T = w ) ) )
91 90 impd 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( ( [ r ] R = [ s ] R /\ [ t ] S = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) -> [ ( r .+ t ) ] T = w ) )
92 eqeq1 
 |-  ( X = [ r ] R -> ( X = [ s ] R <-> [ r ] R = [ s ] R ) )
93 eqeq1 
 |-  ( Y = [ t ] S -> ( Y = [ u ] S <-> [ t ] S = [ u ] S ) )
94 92 93 bi2anan9 
 |-  ( ( X = [ r ] R /\ Y = [ t ] S ) -> ( ( X = [ s ] R /\ Y = [ u ] S ) <-> ( [ r ] R = [ s ] R /\ [ t ] S = [ u ] S ) ) )
95 94 anbi1d 
 |-  ( ( X = [ r ] R /\ Y = [ t ] S ) -> ( ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) <-> ( ( [ r ] R = [ s ] R /\ [ t ] S = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) )
96 95 adantr 
 |-  ( ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) -> ( ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) <-> ( ( [ r ] R = [ s ] R /\ [ t ] S = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) )
97 eqeq1 
 |-  ( z = [ ( r .+ t ) ] T -> ( z = w <-> [ ( r .+ t ) ] T = w ) )
98 97 adantl 
 |-  ( ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) -> ( z = w <-> [ ( r .+ t ) ] T = w ) )
99 96 98 imbi12d 
 |-  ( ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) -> ( ( ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) -> z = w ) <-> ( ( ( [ r ] R = [ s ] R /\ [ t ] S = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) -> [ ( r .+ t ) ] T = w ) ) )
100 91 99 syl5ibrcom 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) -> ( ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) -> z = w ) ) )
101 100 impd 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) -> z = w ) )
102 101 anassrs 
 |-  ( ( ( ph /\ ( r e. A /\ s e. A ) ) /\ ( t e. B /\ u e. B ) ) -> ( ( ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) -> z = w ) )
103 102 rexlimdvva 
 |-  ( ( ph /\ ( r e. A /\ s e. A ) ) -> ( E. t e. B E. u e. B ( ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) -> z = w ) )
104 69 103 syl5bir 
 |-  ( ( ph /\ ( r e. A /\ s e. A ) ) -> ( ( E. t e. B ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ E. u e. B ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) -> z = w ) )
105 104 rexlimdvva 
 |-  ( ph -> ( E. r e. A E. s e. A ( E. t e. B ( ( X = [ r ] R /\ Y = [ t ] S ) /\ z = [ ( r .+ t ) ] T ) /\ E. u e. B ( ( X = [ s ] R /\ Y = [ u ] S ) /\ w = [ ( s .+ u ) ] T ) ) -> z = w ) )
106 68 105 syl5bir 
 |-  ( ph -> ( ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) /\ E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) ) -> z = w ) )
107 106 adantr 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> ( ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) /\ E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) ) -> z = w ) )
108 107 alrimivv 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> A. z A. w ( ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) /\ E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) ) -> z = w ) )
109 eqeq1 
 |-  ( z = w -> ( z = [ ( p .+ q ) ] T <-> w = [ ( p .+ q ) ] T ) )
110 109 anbi2d 
 |-  ( z = w -> ( ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) ) )
111 110 2rexbidv 
 |-  ( z = w -> ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) ) )
112 111 eu4 
 |-  ( E! z E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> ( E. z E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) /\ A. z A. w ( ( E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) /\ E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ w = [ ( p .+ q ) ] T ) ) -> z = w ) ) )
113 35 108 112 sylanbrc 
 |-  ( ( ph /\ ( X e. J /\ Y e. K ) ) -> E! z E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )