Metamath Proof Explorer

Theorem addsasslem1

Description: Lemma for addition associativity. Expand one form of the triple sum. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsasslem.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
addsasslem.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
addsasslem.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
Assertion addsasslem1 ( 𝜑 → ( ( 𝐴 +s 𝐵 ) +s 𝐶 ) = ( ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) } ) ∪ { 𝑤 ∣ ∃ 𝑛 ∈ ( L ‘ 𝐶 ) 𝑤 = ( ( 𝐴 +s 𝐵 ) +s 𝑛 ) } ) |s ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) } ) ∪ { 𝑐 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐶 ) 𝑐 = ( ( 𝐴 +s 𝐵 ) +s 𝑟 ) } ) ) )

Proof

Step Hyp Ref Expression
1 addsasslem.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 addsasslem.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 addsasslem.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 1 2 addscut ⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) <<s { ( 𝐴 +s 𝐵 ) } ∧ { ( 𝐴 +s 𝐵 ) } <<s ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) ) )
5 4 simp2d ⊢ ( 𝜑 → ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) <<s { ( 𝐴 +s 𝐵 ) } )
6 4 simp3d ⊢ ( 𝜑 → { ( 𝐴 +s 𝐵 ) } <<s ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) )
7 ovex ⊢ ( 𝐴 +s 𝐵 ) ∈ V
8 7 snnz ⊢ { ( 𝐴 +s 𝐵 ) } ≠ ∅
9 sslttr ⊢ ( ( ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) <<s { ( 𝐴 +s 𝐵 ) } ∧ { ( 𝐴 +s 𝐵 ) } <<s ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) ∧ { ( 𝐴 +s 𝐵 ) } ≠ ∅ ) → ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) <<s ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) )
10 8 9 mp3an3 ⊢ ( ( ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) <<s { ( 𝐴 +s 𝐵 ) } ∧ { ( 𝐴 +s 𝐵 ) } <<s ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) ) → ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) <<s ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) )
11 5 6 10 syl2anc ⊢ ( 𝜑 → ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) <<s ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) )
12 lltropt ⊢ ( L ‘ 𝐶 ) <<s ( R ‘ 𝐶 )
13 12 a1i ⊢ ( 𝜑 → ( L ‘ 𝐶 ) <<s ( R ‘ 𝐶 ) )
14 addsval2 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) ) )
15 1 2 14 syl2anc ⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) = ( ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) ) )
16 lrcut ⊢ ( 𝐶 ∈ No → ( ( L ‘ 𝐶 ) |s ( R ‘ 𝐶 ) ) = 𝐶 )
17 3 16 syl ⊢ ( 𝜑 → ( ( L ‘ 𝐶 ) |s ( R ‘ 𝐶 ) ) = 𝐶 )
18 17 eqcomd ⊢ ( 𝜑 → 𝐶 = ( ( L ‘ 𝐶 ) |s ( R ‘ 𝐶 ) ) )
19 11 13 15 18 addsunif ⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) +s 𝐶 ) = ( ( { 𝑦 ∣ ∃ ℎ ∈ ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) 𝑦 = ( ℎ +s 𝐶 ) } ∪ { 𝑤 ∣ ∃ 𝑛 ∈ ( L ‘ 𝐶 ) 𝑤 = ( ( 𝐴 +s 𝐵 ) +s 𝑛 ) } ) |s ( { 𝑎 ∣ ∃ 𝑖 ∈ ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) 𝑎 = ( 𝑖 +s 𝐶 ) } ∪ { 𝑐 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐶 ) 𝑐 = ( ( 𝐴 +s 𝐵 ) +s 𝑟 ) } ) ) )
20 unab ⊢ ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑦 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) } ) = { 𝑦 ∣ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) ) }
21 eqeq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) ↔ 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) ) )
22 21 rexbidv ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) ) )
23 22 cbvabv ⊢ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) } = { 𝑦 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) }
24 23 uneq2i ⊢ ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) } ) = ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑦 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) } )
25 rexun ⊢ ( ∃ ℎ ∈ ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) 𝑦 = ( ℎ +s 𝐶 ) ↔ ( ∃ ℎ ∈ { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } 𝑦 = ( ℎ +s 𝐶 ) ∨ ∃ ℎ ∈ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } 𝑦 = ( ℎ +s 𝐶 ) ) )
26 eqeq1 ⊢ ( 𝑑 = ℎ → ( 𝑑 = ( 𝑙 +s 𝐵 ) ↔ ℎ = ( 𝑙 +s 𝐵 ) ) )
27 26 rexbidv ⊢ ( 𝑑 = ℎ → ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ℎ = ( 𝑙 +s 𝐵 ) ) )
28 27 rexab ⊢ ( ∃ ℎ ∈ { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } 𝑦 = ( ℎ +s 𝐶 ) ↔ ∃ ℎ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) )
29 rexcom4 ⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ∃ ℎ ( ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ∃ ℎ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ( ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) )
30 ovex ⊢ ( 𝑙 +s 𝐵 ) ∈ V
31 oveq1 ⊢ ( ℎ = ( 𝑙 +s 𝐵 ) → ( ℎ +s 𝐶 ) = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) )
32 31 eqeq2d ⊢ ( ℎ = ( 𝑙 +s 𝐵 ) → ( 𝑦 = ( ℎ +s 𝐶 ) ↔ 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) ) )
33 30 32 ceqsexv ⊢ ( ∃ ℎ ( ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) )
34 33 rexbii ⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ∃ ℎ ( ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) )
35 r19.41v ⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ( ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) )
36 35 exbii ⊢ ( ∃ ℎ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ( ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ∃ ℎ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) )
37 29 34 36 3bitr3ri ⊢ ( ∃ ℎ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ℎ = ( 𝑙 +s 𝐵 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) )
38 28 37 bitri ⊢ ( ∃ ℎ ∈ { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } 𝑦 = ( ℎ +s 𝐶 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) )
39 eqeq1 ⊢ ( 𝑒 = ℎ → ( 𝑒 = ( 𝐴 +s 𝑚 ) ↔ ℎ = ( 𝐴 +s 𝑚 ) ) )
40 39 rexbidv ⊢ ( 𝑒 = ℎ → ( ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ℎ = ( 𝐴 +s 𝑚 ) ) )
41 40 rexab ⊢ ( ∃ ℎ ∈ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } 𝑦 = ( ℎ +s 𝐶 ) ↔ ∃ ℎ ( ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) )
42 rexcom4 ⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ∃ ℎ ( ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ∃ ℎ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ( ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) )
43 ovex ⊢ ( 𝐴 +s 𝑚 ) ∈ V
44 oveq1 ⊢ ( ℎ = ( 𝐴 +s 𝑚 ) → ( ℎ +s 𝐶 ) = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) )
45 44 eqeq2d ⊢ ( ℎ = ( 𝐴 +s 𝑚 ) → ( 𝑦 = ( ℎ +s 𝐶 ) ↔ 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) ) )
46 43 45 ceqsexv ⊢ ( ∃ ℎ ( ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) )
47 46 rexbii ⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ∃ ℎ ( ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) )
48 r19.41v ⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ( ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ( ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) )
49 48 exbii ⊢ ( ∃ ℎ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ( ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ∃ ℎ ( ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) )
50 42 47 49 3bitr3ri ⊢ ( ∃ ℎ ( ∃ 𝑚 ∈ ( L ‘ 𝐵 ) ℎ = ( 𝐴 +s 𝑚 ) ∧ 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) )
51 41 50 bitri ⊢ ( ∃ ℎ ∈ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } 𝑦 = ( ℎ +s 𝐶 ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) )
52 38 51 orbi12i ⊢ ( ( ∃ ℎ ∈ { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } 𝑦 = ( ℎ +s 𝐶 ) ∨ ∃ ℎ ∈ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } 𝑦 = ( ℎ +s 𝐶 ) ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) ) )
53 25 52 bitri ⊢ ( ∃ ℎ ∈ ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) 𝑦 = ( ℎ +s 𝐶 ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) ) )
54 53 abbii ⊢ { 𝑦 ∣ ∃ ℎ ∈ ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) 𝑦 = ( ℎ +s 𝐶 ) } = { 𝑦 ∣ ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) ) }
55 20 24 54 3eqtr4ri ⊢ { 𝑦 ∣ ∃ ℎ ∈ ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) 𝑦 = ( ℎ +s 𝐶 ) } = ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) } )
56 55 uneq1i ⊢ ( { 𝑦 ∣ ∃ ℎ ∈ ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) 𝑦 = ( ℎ +s 𝐶 ) } ∪ { 𝑤 ∣ ∃ 𝑛 ∈ ( L ‘ 𝐶 ) 𝑤 = ( ( 𝐴 +s 𝐵 ) +s 𝑛 ) } ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) } ) ∪ { 𝑤 ∣ ∃ 𝑛 ∈ ( L ‘ 𝐶 ) 𝑤 = ( ( 𝐴 +s 𝐵 ) +s 𝑛 ) } )
57 unab ⊢ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑎 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) } ) = { 𝑎 ∣ ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) ∨ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) ) }
58 eqeq1 ⊢ ( 𝑏 = 𝑎 → ( 𝑏 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) ↔ 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) ) )
59 58 rexbidv ⊢ ( 𝑏 = 𝑎 → ( ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) ↔ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) ) )
60 59 cbvabv ⊢ { 𝑏 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) } = { 𝑎 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) }
61 60 uneq2i ⊢ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) } ) = ( { 𝑎 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑎 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) } )
62 rexun ⊢ ( ∃ 𝑖 ∈ ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) 𝑎 = ( 𝑖 +s 𝐶 ) ↔ ( ∃ 𝑖 ∈ { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } 𝑎 = ( 𝑖 +s 𝐶 ) ∨ ∃ 𝑖 ∈ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } 𝑎 = ( 𝑖 +s 𝐶 ) ) )
63 eqeq1 ⊢ ( 𝑓 = 𝑖 → ( 𝑓 = ( 𝑝 +s 𝐵 ) ↔ 𝑖 = ( 𝑝 +s 𝐵 ) ) )
64 63 rexbidv ⊢ ( 𝑓 = 𝑖 → ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) ↔ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑖 = ( 𝑝 +s 𝐵 ) ) )
65 64 rexab ⊢ ( ∃ 𝑖 ∈ { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } 𝑎 = ( 𝑖 +s 𝐶 ) ↔ ∃ 𝑖 ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) )
66 rexcom4 ⊢ ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) ∃ 𝑖 ( 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ∃ 𝑖 ∃ 𝑝 ∈ ( R ‘ 𝐴 ) ( 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) )
67 ovex ⊢ ( 𝑝 +s 𝐵 ) ∈ V
68 oveq1 ⊢ ( 𝑖 = ( 𝑝 +s 𝐵 ) → ( 𝑖 +s 𝐶 ) = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) )
69 68 eqeq2d ⊢ ( 𝑖 = ( 𝑝 +s 𝐵 ) → ( 𝑎 = ( 𝑖 +s 𝐶 ) ↔ 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) ) )
70 67 69 ceqsexv ⊢ ( ∃ 𝑖 ( 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) )
71 70 rexbii ⊢ ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) ∃ 𝑖 ( 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) )
72 r19.41v ⊢ ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) ( 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) )
73 72 exbii ⊢ ( ∃ 𝑖 ∃ 𝑝 ∈ ( R ‘ 𝐴 ) ( 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ∃ 𝑖 ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) )
74 66 71 73 3bitr3ri ⊢ ( ∃ 𝑖 ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑖 = ( 𝑝 +s 𝐵 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) )
75 65 74 bitri ⊢ ( ∃ 𝑖 ∈ { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } 𝑎 = ( 𝑖 +s 𝐶 ) ↔ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) )
76 eqeq1 ⊢ ( 𝑔 = 𝑖 → ( 𝑔 = ( 𝐴 +s 𝑞 ) ↔ 𝑖 = ( 𝐴 +s 𝑞 ) ) )
77 76 rexbidv ⊢ ( 𝑔 = 𝑖 → ( ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) ↔ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑖 = ( 𝐴 +s 𝑞 ) ) )
78 77 rexab ⊢ ( ∃ 𝑖 ∈ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } 𝑎 = ( 𝑖 +s 𝐶 ) ↔ ∃ 𝑖 ( ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) )
79 rexcom4 ⊢ ( ∃ 𝑞 ∈ ( R ‘ 𝐵 ) ∃ 𝑖 ( 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ∃ 𝑖 ∃ 𝑞 ∈ ( R ‘ 𝐵 ) ( 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) )
80 ovex ⊢ ( 𝐴 +s 𝑞 ) ∈ V
81 oveq1 ⊢ ( 𝑖 = ( 𝐴 +s 𝑞 ) → ( 𝑖 +s 𝐶 ) = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) )
82 81 eqeq2d ⊢ ( 𝑖 = ( 𝐴 +s 𝑞 ) → ( 𝑎 = ( 𝑖 +s 𝐶 ) ↔ 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) ) )
83 80 82 ceqsexv ⊢ ( ∃ 𝑖 ( 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) )
84 83 rexbii ⊢ ( ∃ 𝑞 ∈ ( R ‘ 𝐵 ) ∃ 𝑖 ( 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) )
85 r19.41v ⊢ ( ∃ 𝑞 ∈ ( R ‘ 𝐵 ) ( 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ( ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) )
86 85 exbii ⊢ ( ∃ 𝑖 ∃ 𝑞 ∈ ( R ‘ 𝐵 ) ( 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ∃ 𝑖 ( ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) )
87 79 84 86 3bitr3ri ⊢ ( ∃ 𝑖 ( ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑖 = ( 𝐴 +s 𝑞 ) ∧ 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) )
88 78 87 bitri ⊢ ( ∃ 𝑖 ∈ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } 𝑎 = ( 𝑖 +s 𝐶 ) ↔ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) )
89 75 88 orbi12i ⊢ ( ( ∃ 𝑖 ∈ { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } 𝑎 = ( 𝑖 +s 𝐶 ) ∨ ∃ 𝑖 ∈ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } 𝑎 = ( 𝑖 +s 𝐶 ) ) ↔ ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) ∨ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) ) )
90 62 89 bitri ⊢ ( ∃ 𝑖 ∈ ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) 𝑎 = ( 𝑖 +s 𝐶 ) ↔ ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) ∨ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) ) )
91 90 abbii ⊢ { 𝑎 ∣ ∃ 𝑖 ∈ ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) 𝑎 = ( 𝑖 +s 𝐶 ) } = { 𝑎 ∣ ( ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) ∨ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) ) }
92 57 61 91 3eqtr4ri ⊢ { 𝑎 ∣ ∃ 𝑖 ∈ ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) 𝑎 = ( 𝑖 +s 𝐶 ) } = ( { 𝑎 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) } )
93 92 uneq1i ⊢ ( { 𝑎 ∣ ∃ 𝑖 ∈ ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) 𝑎 = ( 𝑖 +s 𝐶 ) } ∪ { 𝑐 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐶 ) 𝑐 = ( ( 𝐴 +s 𝐵 ) +s 𝑟 ) } ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) } ) ∪ { 𝑐 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐶 ) 𝑐 = ( ( 𝐴 +s 𝐵 ) +s 𝑟 ) } )
94 56 93 oveq12i ⊢ ( ( { 𝑦 ∣ ∃ ℎ ∈ ( { 𝑑 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑑 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑒 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑒 = ( 𝐴 +s 𝑚 ) } ) 𝑦 = ( ℎ +s 𝐶 ) } ∪ { 𝑤 ∣ ∃ 𝑛 ∈ ( L ‘ 𝐶 ) 𝑤 = ( ( 𝐴 +s 𝐵 ) +s 𝑛 ) } ) |s ( { 𝑎 ∣ ∃ 𝑖 ∈ ( { 𝑓 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑓 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑔 = ( 𝐴 +s 𝑞 ) } ) 𝑎 = ( 𝑖 +s 𝐶 ) } ∪ { 𝑐 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐶 ) 𝑐 = ( ( 𝐴 +s 𝐵 ) +s 𝑟 ) } ) ) = ( ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) } ) ∪ { 𝑤 ∣ ∃ 𝑛 ∈ ( L ‘ 𝐶 ) 𝑤 = ( ( 𝐴 +s 𝐵 ) +s 𝑛 ) } ) |s ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) } ) ∪ { 𝑐 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐶 ) 𝑐 = ( ( 𝐴 +s 𝐵 ) +s 𝑟 ) } ) )
95 19 94 eqtrdi ⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) +s 𝐶 ) = ( ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( ( 𝑙 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( ( 𝐴 +s 𝑚 ) +s 𝐶 ) } ) ∪ { 𝑤 ∣ ∃ 𝑛 ∈ ( L ‘ 𝐶 ) 𝑤 = ( ( 𝐴 +s 𝐵 ) +s 𝑛 ) } ) |s ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( R ‘ 𝐴 ) 𝑎 = ( ( 𝑝 +s 𝐵 ) +s 𝐶 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( 𝐴 +s 𝑞 ) +s 𝐶 ) } ) ∪ { 𝑐 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐶 ) 𝑐 = ( ( 𝐴 +s 𝐵 ) +s 𝑟 ) } ) ) )