Metamath Proof Explorer

Theorem erovlem

Description: Lemma for erov and eroprf . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-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 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠 ∧ 𝑡 𝑆 𝑢 ) → ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ) )
eropr.12 ⊢ ⨣ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) }
Assertion erovlem ( 𝜑 → ⨣ = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )

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 eropr.12 ⊢ ⨣ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) }
13 simpl ⊢ ( ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) )
14 13 reximi ⊢ ( ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ∃ 𝑞 ∈ 𝐵 ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) )
15 14 reximi ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) )
16 1 eleq2i ⊢ ( 𝑥 ∈ 𝐽 ↔ 𝑥 ∈ ( 𝐴 / 𝑅 ) )
17 vex ⊢ 𝑥 ∈ V
18 17 elqs ⊢ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑝 ∈ 𝐴 𝑥 = [ 𝑝 ] 𝑅 )
19 16 18 bitri ⊢ ( 𝑥 ∈ 𝐽 ↔ ∃ 𝑝 ∈ 𝐴 𝑥 = [ 𝑝 ] 𝑅 )
20 2 eleq2i ⊢ ( 𝑦 ∈ 𝐾 ↔ 𝑦 ∈ ( 𝐵 / 𝑆 ) )
21 vex ⊢ 𝑦 ∈ V
22 21 elqs ⊢ ( 𝑦 ∈ ( 𝐵 / 𝑆 ) ↔ ∃ 𝑞 ∈ 𝐵 𝑦 = [ 𝑞 ] 𝑆 )
23 20 22 bitri ⊢ ( 𝑦 ∈ 𝐾 ↔ ∃ 𝑞 ∈ 𝐵 𝑦 = [ 𝑞 ] 𝑆 )
24 19 23 anbi12i ⊢ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ↔ ( ∃ 𝑝 ∈ 𝐴 𝑥 = [ 𝑝 ] 𝑅 ∧ ∃ 𝑞 ∈ 𝐵 𝑦 = [ 𝑞 ] 𝑆 ) )
25 reeanv ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ↔ ( ∃ 𝑝 ∈ 𝐴 𝑥 = [ 𝑝 ] 𝑅 ∧ ∃ 𝑞 ∈ 𝐵 𝑦 = [ 𝑞 ] 𝑆 ) )
26 24 25 bitr4i ⊢ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) )
27 15 26 sylibr ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) )
28 27 pm4.71ri ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
29 1 2 3 4 5 6 7 8 9 10 11 eroveu ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ∃! 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
30 iota1 ⊢ ( ∃! 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) = 𝑧 ) )
31 29 30 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) = 𝑧 ) )
32 eqcom ⊢ ( ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) = 𝑧 ↔ 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
33 31 32 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )
34 33 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ↔ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) ) )
35 28 34 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) ) )
36 35 oprabbidv ⊢ ( 𝜑 → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) } )
37 df-mpo ⊢ ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑤 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) }
38 nfv ⊢ Ⅎ 𝑤 ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
39 nfv ⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 )
40 nfiota1 ⊢ Ⅎ 𝑧 ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
41 40 nfeq2 ⊢ Ⅎ 𝑧 𝑤 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
42 39 41 nfan ⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑤 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
43 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ↔ 𝑤 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )
44 43 anbi2d ⊢ ( 𝑧 = 𝑤 → ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) ↔ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑤 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) ) )
45 38 42 44 cbvoprab3 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑤 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) }
46 37 45 eqtr4i ⊢ ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) }
47 36 12 46 3eqtr4g ⊢ ( 𝜑 → ⨣ = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )