This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( 𝐴 / 𝑅 )
eropr.2 ⊢ 𝐾 = ( 𝐵 / 𝑆 )
eropr.3 ⊢ ( 𝜑 → 𝑇 ∈ 𝑍 )
eropr.4 ⊢ ( 𝜑 → 𝑅 Er 𝑈 )
eropr.5 ⊢ ( 𝜑 → 𝑆 Er 𝑉 )
eropr.6 ⊢ ( 𝜑 → 𝑇 Er 𝑊 )
eropr.7 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
eropr.8 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑉 )
eropr.9 ⊢ ( 𝜑 → 𝐶 ⊆ 𝑊 )
eropr.10 ⊢ ( 𝜑 → + : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
eropr.11 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠 ∧ 𝑡 𝑆 𝑢 ) → ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ) )
Assertion eroveu ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ∃! 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )

Proof

Step Hyp Ref Expression
1 eropr.1 ⊢ 𝐽 = ( 𝐴 / 𝑅 )
2 eropr.2 ⊢ 𝐾 = ( 𝐵 / 𝑆 )
3 eropr.3 ⊢ ( 𝜑 → 𝑇 ∈ 𝑍 )
4 eropr.4 ⊢ ( 𝜑 → 𝑅 Er 𝑈 )
5 eropr.5 ⊢ ( 𝜑 → 𝑆 Er 𝑉 )
6 eropr.6 ⊢ ( 𝜑 → 𝑇 Er 𝑊 )
7 eropr.7 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
8 eropr.8 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑉 )
9 eropr.9 ⊢ ( 𝜑 → 𝐶 ⊆ 𝑊 )
10 eropr.10 ⊢ ( 𝜑 → + : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
11 eropr.11 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠 ∧ 𝑡 𝑆 𝑢 ) → ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ) )
12 elqsi ⊢ ( 𝑋 ∈ ( 𝐴 / 𝑅 ) → ∃ 𝑝 ∈ 𝐴 𝑋 = [ 𝑝 ] 𝑅 )
13 12 1 eleq2s ⊢ ( 𝑋 ∈ 𝐽 → ∃ 𝑝 ∈ 𝐴 𝑋 = [ 𝑝 ] 𝑅 )
14 elqsi ⊢ ( 𝑌 ∈ ( 𝐵 / 𝑆 ) → ∃ 𝑞 ∈ 𝐵 𝑌 = [ 𝑞 ] 𝑆 )
15 14 2 eleq2s ⊢ ( 𝑌 ∈ 𝐾 → ∃ 𝑞 ∈ 𝐵 𝑌 = [ 𝑞 ] 𝑆 )
16 13 15 anim12i ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) → ( ∃ 𝑝 ∈ 𝐴 𝑋 = [ 𝑝 ] 𝑅 ∧ ∃ 𝑞 ∈ 𝐵 𝑌 = [ 𝑞 ] 𝑆 ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ( ∃ 𝑝 ∈ 𝐴 𝑋 = [ 𝑝 ] 𝑅 ∧ ∃ 𝑞 ∈ 𝐵 𝑌 = [ 𝑞 ] 𝑆 ) )
18 reeanv ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ↔ ( ∃ 𝑝 ∈ 𝐴 𝑋 = [ 𝑝 ] 𝑅 ∧ ∃ 𝑞 ∈ 𝐵 𝑌 = [ 𝑞 ] 𝑆 ) )
19 17 18 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) )
20 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → 𝑇 ∈ 𝑍 )
21 ecexg ⊢ ( 𝑇 ∈ 𝑍 → [ ( 𝑝 + 𝑞 ) ] 𝑇 ∈ V )
22 elisset ⊢ ( [ ( 𝑝 + 𝑞 ) ] 𝑇 ∈ V → ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 )
23 20 21 22 3syl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 )
24 23 biantrud ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ↔ ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
25 24 2rexbidv ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
26 19 25 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
27 19.42v ⊢ ( ∃ 𝑧 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
28 27 bicomi ⊢ ( ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑧 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
29 28 rexbii ⊢ ( ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑞 ∈ 𝐵 ∃ 𝑧 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
30 rexcom4 ⊢ ( ∃ 𝑞 ∈ 𝐵 ∃ 𝑧 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑧 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
31 29 30 bitri ⊢ ( ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑧 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
32 31 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑧 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
33 rexcom4 ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑧 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
34 32 33 bitri ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ ∃ 𝑧 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
35 26 34 sylib ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ∃ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
36 reeanv ⊢ ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ∃ 𝑡 ∈ 𝐵 ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ∃ 𝑢 ∈ 𝐵 ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) ↔ ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑡 ∈ 𝐵 ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ∃ 𝑠 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) )
37 eceq1 ⊢ ( 𝑝 = 𝑟 → [ 𝑝 ] 𝑅 = [ 𝑟 ] 𝑅 )
38 37 eqeq2d ⊢ ( 𝑝 = 𝑟 → ( 𝑋 = [ 𝑝 ] 𝑅 ↔ 𝑋 = [ 𝑟 ] 𝑅 ) )
39 38 anbi1d ⊢ ( 𝑝 = 𝑟 → ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ↔ ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ) )
40 oveq1 ⊢ ( 𝑝 = 𝑟 → ( 𝑝 + 𝑞 ) = ( 𝑟 + 𝑞 ) )
41 40 eceq1d ⊢ ( 𝑝 = 𝑟 → [ ( 𝑝 + 𝑞 ) ] 𝑇 = [ ( 𝑟 + 𝑞 ) ] 𝑇 )
42 41 eqeq2d ⊢ ( 𝑝 = 𝑟 → ( 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ↔ 𝑧 = [ ( 𝑟 + 𝑞 ) ] 𝑇 ) )
43 39 42 anbi12d ⊢ ( 𝑝 = 𝑟 → ( ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑞 ) ] 𝑇 ) ) )
44 eceq1 ⊢ ( 𝑞 = 𝑡 → [ 𝑞 ] 𝑆 = [ 𝑡 ] 𝑆 )
45 44 eqeq2d ⊢ ( 𝑞 = 𝑡 → ( 𝑌 = [ 𝑞 ] 𝑆 ↔ 𝑌 = [ 𝑡 ] 𝑆 ) )
46 45 anbi2d ⊢ ( 𝑞 = 𝑡 → ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ↔ ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ) )
47 oveq2 ⊢ ( 𝑞 = 𝑡 → ( 𝑟 + 𝑞 ) = ( 𝑟 + 𝑡 ) )
48 47 eceq1d ⊢ ( 𝑞 = 𝑡 → [ ( 𝑟 + 𝑞 ) ] 𝑇 = [ ( 𝑟 + 𝑡 ) ] 𝑇 )
49 48 eqeq2d ⊢ ( 𝑞 = 𝑡 → ( 𝑧 = [ ( 𝑟 + 𝑞 ) ] 𝑇 ↔ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) )
50 46 49 anbi12d ⊢ ( 𝑞 = 𝑡 → ( ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ) )
51 43 50 cbvrex2vw ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑡 ∈ 𝐵 ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) )
52 eceq1 ⊢ ( 𝑝 = 𝑠 → [ 𝑝 ] 𝑅 = [ 𝑠 ] 𝑅 )
53 52 eqeq2d ⊢ ( 𝑝 = 𝑠 → ( 𝑋 = [ 𝑝 ] 𝑅 ↔ 𝑋 = [ 𝑠 ] 𝑅 ) )
54 53 anbi1d ⊢ ( 𝑝 = 𝑠 → ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ↔ ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ) )
55 oveq1 ⊢ ( 𝑝 = 𝑠 → ( 𝑝 + 𝑞 ) = ( 𝑠 + 𝑞 ) )
56 55 eceq1d ⊢ ( 𝑝 = 𝑠 → [ ( 𝑝 + 𝑞 ) ] 𝑇 = [ ( 𝑠 + 𝑞 ) ] 𝑇 )
57 56 eqeq2d ⊢ ( 𝑝 = 𝑠 → ( 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ↔ 𝑤 = [ ( 𝑠 + 𝑞 ) ] 𝑇 ) )
58 54 57 anbi12d ⊢ ( 𝑝 = 𝑠 → ( ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑞 ) ] 𝑇 ) ) )
59 eceq1 ⊢ ( 𝑞 = 𝑢 → [ 𝑞 ] 𝑆 = [ 𝑢 ] 𝑆 )
60 59 eqeq2d ⊢ ( 𝑞 = 𝑢 → ( 𝑌 = [ 𝑞 ] 𝑆 ↔ 𝑌 = [ 𝑢 ] 𝑆 ) )
61 60 anbi2d ⊢ ( 𝑞 = 𝑢 → ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ↔ ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ) )
62 oveq2 ⊢ ( 𝑞 = 𝑢 → ( 𝑠 + 𝑞 ) = ( 𝑠 + 𝑢 ) )
63 62 eceq1d ⊢ ( 𝑞 = 𝑢 → [ ( 𝑠 + 𝑞 ) ] 𝑇 = [ ( 𝑠 + 𝑢 ) ] 𝑇 )
64 63 eqeq2d ⊢ ( 𝑞 = 𝑢 → ( 𝑤 = [ ( 𝑠 + 𝑞 ) ] 𝑇 ↔ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) )
65 61 64 anbi12d ⊢ ( 𝑞 = 𝑢 → ( ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) )
66 58 65 cbvrex2vw ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑠 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) )
67 51 66 anbi12i ⊢ ( ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ↔ ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑡 ∈ 𝐵 ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ∃ 𝑠 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) )
68 36 67 bitr4i ⊢ ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ∃ 𝑡 ∈ 𝐵 ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ∃ 𝑢 ∈ 𝐵 ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) ↔ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
69 reeanv ⊢ ( ∃ 𝑡 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) ↔ ( ∃ 𝑡 ∈ 𝐵 ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ∃ 𝑢 ∈ 𝐵 ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) )
70 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑅 Er 𝑈 )
71 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝐴 ⊆ 𝑈 )
72 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑟 ∈ 𝐴 )
73 71 72 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑟 ∈ 𝑈 )
74 70 73 erth ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( 𝑟 𝑅 𝑠 ↔ [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ) )
75 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑆 Er 𝑉 )
76 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝐵 ⊆ 𝑉 )
77 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑡 ∈ 𝐵 )
78 76 77 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑡 ∈ 𝑉 )
79 75 78 erth ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( 𝑡 𝑆 𝑢 ↔ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) )
80 74 79 anbi12d ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠 ∧ 𝑡 𝑆 𝑢 ) ↔ ( [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ∧ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) ) )
81 6 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑇 Er 𝑊 )
82 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝐶 ⊆ 𝑊 )
83 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → + : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
84 83 72 77 fovcdmd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( 𝑟 + 𝑡 ) ∈ 𝐶 )
85 82 84 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( 𝑟 + 𝑡 ) ∈ 𝑊 )
86 81 85 erth ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ↔ [ ( 𝑟 + 𝑡 ) ] 𝑇 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) )
87 11 80 86 3imtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ∧ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) → [ ( 𝑟 + 𝑡 ) ] 𝑇 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) )
88 eqeq2 ⊢ ( 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 → ( [ ( 𝑟 + 𝑡 ) ] 𝑇 = 𝑤 ↔ [ ( 𝑟 + 𝑡 ) ] 𝑇 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) )
89 88 biimprcd ⊢ ( [ ( 𝑟 + 𝑡 ) ] 𝑇 = [ ( 𝑠 + 𝑢 ) ] 𝑇 → ( 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 → [ ( 𝑟 + 𝑡 ) ] 𝑇 = 𝑤 ) )
90 87 89 syl6 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ∧ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) → ( 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 → [ ( 𝑟 + 𝑡 ) ] 𝑇 = 𝑤 ) ) )
91 90 impd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( ( [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ∧ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) → [ ( 𝑟 + 𝑡 ) ] 𝑇 = 𝑤 ) )
92 eqeq1 ⊢ ( 𝑋 = [ 𝑟 ] 𝑅 → ( 𝑋 = [ 𝑠 ] 𝑅 ↔ [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ) )
93 eqeq1 ⊢ ( 𝑌 = [ 𝑡 ] 𝑆 → ( 𝑌 = [ 𝑢 ] 𝑆 ↔ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) )
94 92 93 bi2anan9 ⊢ ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) → ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ↔ ( [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ∧ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) ) )
95 94 anbi1d ⊢ ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) → ( ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ↔ ( ( [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ∧ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) )
96 95 adantr ⊢ ( ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) → ( ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ↔ ( ( [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ∧ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) )
97 eqeq1 ⊢ ( 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 → ( 𝑧 = 𝑤 ↔ [ ( 𝑟 + 𝑡 ) ] 𝑇 = 𝑤 ) )
98 97 adantl ⊢ ( ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) → ( 𝑧 = 𝑤 ↔ [ ( 𝑟 + 𝑡 ) ] 𝑇 = 𝑤 ) )
99 96 98 imbi12d ⊢ ( ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) → ( ( ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) → 𝑧 = 𝑤 ) ↔ ( ( ( [ 𝑟 ] 𝑅 = [ 𝑠 ] 𝑅 ∧ [ 𝑡 ] 𝑆 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) → [ ( 𝑟 + 𝑡 ) ] 𝑇 = 𝑤 ) ) )
100 91 99 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) → ( ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) → 𝑧 = 𝑤 ) ) )
101 100 impd ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) → 𝑧 = 𝑤 ) )
102 101 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → ( ( ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) → 𝑧 = 𝑤 ) )
103 102 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) → ( ∃ 𝑡 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) → 𝑧 = 𝑤 ) )
104 69 103 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) → ( ( ∃ 𝑡 ∈ 𝐵 ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ∃ 𝑢 ∈ 𝐵 ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) → 𝑧 = 𝑤 ) )
105 104 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ∃ 𝑡 ∈ 𝐵 ( ( 𝑋 = [ 𝑟 ] 𝑅 ∧ 𝑌 = [ 𝑡 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑟 + 𝑡 ) ] 𝑇 ) ∧ ∃ 𝑢 ∈ 𝐵 ( ( 𝑋 = [ 𝑠 ] 𝑅 ∧ 𝑌 = [ 𝑢 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑠 + 𝑢 ) ] 𝑇 ) ) → 𝑧 = 𝑤 ) )
106 68 105 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) → 𝑧 = 𝑤 ) )
107 106 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ( ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) → 𝑧 = 𝑤 ) )
108 107 alrimivv ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ∀ 𝑧 ∀ 𝑤 ( ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) → 𝑧 = 𝑤 ) )
109 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ↔ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
110 109 anbi2d ⊢ ( 𝑧 = 𝑤 → ( ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
111 110 2rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
112 111 eu4 ⊢ ( ∃! 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ∃ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑤 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) → 𝑧 = 𝑤 ) ) )
113 35 108 112 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ∃! 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑋 = [ 𝑝 ] 𝑅 ∧ 𝑌 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )