Metamath Proof Explorer

Theorem addsasslem2

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