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 bitrid âŠĒ ( 𝜑 → ( ∃ 𝑝 ∈ ðī ∃ 𝑞 ∈ ðĩ ( ( ð‘Ĩ = [ 𝑝 ] 𝑅 ∧ ð‘Ķ = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( ð‘Ĩ ∈ ð― ∧ ð‘Ķ ∈ ðū ) ∧ 𝑧 = ( â„Đ 𝑧 ∃ 𝑝 ∈ ðī ∃ 𝑞 ∈ ðĩ ( ( ð‘Ĩ = [ 𝑝 ] 𝑅 ∧ ð‘Ķ = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) ) )
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 âŠĒ ( 𝜑 → âĻĢ = ( ð‘Ĩ ∈ ð― , ð‘Ķ ∈ ðū â†Ķ ( â„Đ 𝑧 ∃ 𝑝 ∈ ðī ∃ 𝑞 ∈ ðĩ ( ( ð‘Ĩ = [ 𝑝 ] 𝑅 ∧ ð‘Ķ = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )