Metamath Proof Explorer

Theorem addsass

Description: Surreal addition is associative. Part of theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 22-Jan-2025)

Ref Expression
Assertion addsass ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐴 +s 𝐵 ) +s 𝐶 ) = ( 𝐴 +s ( 𝐵 +s 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑥 = 𝑥𝑂 → ( 𝑥 +s 𝑦 ) = ( 𝑥𝑂 +s 𝑦 ) )
2 1 oveq1d ⊢ ( 𝑥 = 𝑥𝑂 → ( ( 𝑥 +s 𝑦 ) +s 𝑧 ) = ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) )
3 oveq1 ⊢ ( 𝑥 = 𝑥𝑂 → ( 𝑥 +s ( 𝑦 +s 𝑧 ) ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) )
4 2 3 eqeq12d ⊢ ( 𝑥 = 𝑥𝑂 → ( ( ( 𝑥 +s 𝑦 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦 +s 𝑧 ) ) ↔ ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ) )
5 oveq2 ⊢ ( 𝑦 = 𝑦𝑂 → ( 𝑥𝑂 +s 𝑦 ) = ( 𝑥𝑂 +s 𝑦𝑂 ) )
6 5 oveq1d ⊢ ( 𝑦 = 𝑦𝑂 → ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧 ) )
7 oveq1 ⊢ ( 𝑦 = 𝑦𝑂 → ( 𝑦 +s 𝑧 ) = ( 𝑦𝑂 +s 𝑧 ) )
8 7 oveq2d ⊢ ( 𝑦 = 𝑦𝑂 → ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧 ) ) )
9 6 8 eqeq12d ⊢ ( 𝑦 = 𝑦𝑂 → ( ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ↔ ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧 ) ) ) )
10 oveq2 ⊢ ( 𝑧 = 𝑧𝑂 → ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧 ) = ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) )
11 oveq2 ⊢ ( 𝑧 = 𝑧𝑂 → ( 𝑦𝑂 +s 𝑧 ) = ( 𝑦𝑂 +s 𝑧𝑂 ) )
12 11 oveq2d ⊢ ( 𝑧 = 𝑧𝑂 → ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧 ) ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
13 10 12 eqeq12d ⊢ ( 𝑧 = 𝑧𝑂 → ( ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧 ) ) ↔ ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ) )
14 oveq1 ⊢ ( 𝑥 = 𝑥𝑂 → ( 𝑥 +s 𝑦𝑂 ) = ( 𝑥𝑂 +s 𝑦𝑂 ) )
15 14 oveq1d ⊢ ( 𝑥 = 𝑥𝑂 → ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) )
16 oveq1 ⊢ ( 𝑥 = 𝑥𝑂 → ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
17 15 16 eqeq12d ⊢ ( 𝑥 = 𝑥𝑂 → ( ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ↔ ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ) )
18 oveq2 ⊢ ( 𝑦 = 𝑦𝑂 → ( 𝑥 +s 𝑦 ) = ( 𝑥 +s 𝑦𝑂 ) )
19 18 oveq1d ⊢ ( 𝑦 = 𝑦𝑂 → ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) )
20 oveq1 ⊢ ( 𝑦 = 𝑦𝑂 → ( 𝑦 +s 𝑧𝑂 ) = ( 𝑦𝑂 +s 𝑧𝑂 ) )
21 20 oveq2d ⊢ ( 𝑦 = 𝑦𝑂 → ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
22 19 21 eqeq12d ⊢ ( 𝑦 = 𝑦𝑂 → ( ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ↔ ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ) )
23 5 oveq1d ⊢ ( 𝑦 = 𝑦𝑂 → ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧𝑂 ) = ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) )
24 20 oveq2d ⊢ ( 𝑦 = 𝑦𝑂 → ( 𝑥𝑂 +s ( 𝑦 +s 𝑧𝑂 ) ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
25 23 24 eqeq12d ⊢ ( 𝑦 = 𝑦𝑂 → ( ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧𝑂 ) ) ↔ ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ) )
26 oveq2 ⊢ ( 𝑧 = 𝑧𝑂 → ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) )
27 11 oveq2d ⊢ ( 𝑧 = 𝑧𝑂 → ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
28 26 27 eqeq12d ⊢ ( 𝑧 = 𝑧𝑂 → ( ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ↔ ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ) )
29 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 +s 𝑦 ) = ( 𝐴 +s 𝑦 ) )
30 29 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 +s 𝑦 ) +s 𝑧 ) = ( ( 𝐴 +s 𝑦 ) +s 𝑧 ) )
31 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 +s ( 𝑦 +s 𝑧 ) ) = ( 𝐴 +s ( 𝑦 +s 𝑧 ) ) )
32 30 31 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 +s 𝑦 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦 +s 𝑧 ) ) ↔ ( ( 𝐴 +s 𝑦 ) +s 𝑧 ) = ( 𝐴 +s ( 𝑦 +s 𝑧 ) ) ) )
33 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 +s 𝑦 ) = ( 𝐴 +s 𝐵 ) )
34 33 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 +s 𝑦 ) +s 𝑧 ) = ( ( 𝐴 +s 𝐵 ) +s 𝑧 ) )
35 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 +s 𝑧 ) = ( 𝐵 +s 𝑧 ) )
36 35 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 +s ( 𝑦 +s 𝑧 ) ) = ( 𝐴 +s ( 𝐵 +s 𝑧 ) ) )
37 34 36 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 +s 𝑦 ) +s 𝑧 ) = ( 𝐴 +s ( 𝑦 +s 𝑧 ) ) ↔ ( ( 𝐴 +s 𝐵 ) +s 𝑧 ) = ( 𝐴 +s ( 𝐵 +s 𝑧 ) ) ) )
38 oveq2 ⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 +s 𝐵 ) +s 𝑧 ) = ( ( 𝐴 +s 𝐵 ) +s 𝐶 ) )
39 oveq2 ⊢ ( 𝑧 = 𝐶 → ( 𝐵 +s 𝑧 ) = ( 𝐵 +s 𝐶 ) )
40 39 oveq2d ⊢ ( 𝑧 = 𝐶 → ( 𝐴 +s ( 𝐵 +s 𝑧 ) ) = ( 𝐴 +s ( 𝐵 +s 𝐶 ) ) )
41 38 40 eqeq12d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 +s 𝐵 ) +s 𝑧 ) = ( 𝐴 +s ( 𝐵 +s 𝑧 ) ) ↔ ( ( 𝐴 +s 𝐵 ) +s 𝐶 ) = ( 𝐴 +s ( 𝐵 +s 𝐶 ) ) ) )
42 simp21 ⊢ ( ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) )
43 simp23 ⊢ ( ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) )
44 simp3 ⊢ ( ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) → ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) )
45 42 43 44 3jca ⊢ ( ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) → ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) )
46 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 𝑥𝑂 +s 𝑦 ) = ( 𝑥𝐿 +s 𝑦 ) )
47 46 oveq1d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) )
48 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) = ( 𝑥𝐿 +s ( 𝑦 +s 𝑧 ) ) )
49 47 48 eqeq12d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ↔ ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝐿 +s ( 𝑦 +s 𝑧 ) ) ) )
50 simplr1 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) )
51 elun1 ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
52 51 adantl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
53 49 50 52 rspcdva ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝐿 +s ( 𝑦 +s 𝑧 ) ) )
54 53 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑎 = ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) ↔ 𝑎 = ( 𝑥𝐿 +s ( 𝑦 +s 𝑧 ) ) ) )
55 54 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( 𝑦 +s 𝑧 ) ) ) )
56 55 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) } = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( 𝑦 +s 𝑧 ) ) } )
57 oveq2 ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( 𝑥 +s 𝑦𝑂 ) = ( 𝑥 +s 𝑦𝐿 ) )
58 57 oveq1d ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) )
59 oveq1 ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( 𝑦𝑂 +s 𝑧 ) = ( 𝑦𝐿 +s 𝑧 ) )
60 59 oveq2d ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) = ( 𝑥 +s ( 𝑦𝐿 +s 𝑧 ) ) )
61 58 60 eqeq12d ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ↔ ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝐿 +s 𝑧 ) ) ) )
62 simplr2 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) )
63 elun1 ⊢ ( 𝑦𝐿 ∈ ( L ‘ 𝑦 ) → 𝑦𝐿 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
64 63 adantl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) → 𝑦𝐿 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
65 61 62 64 rspcdva ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) → ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝐿 +s 𝑧 ) ) )
66 65 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) → ( 𝑏 = ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) ↔ 𝑏 = ( 𝑥 +s ( 𝑦𝐿 +s 𝑧 ) ) ) )
67 66 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) ↔ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( 𝑥 +s ( 𝑦𝐿 +s 𝑧 ) ) ) )
68 67 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → { 𝑏 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) } = { 𝑏 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( 𝑥 +s ( 𝑦𝐿 +s 𝑧 ) ) } )
69 56 68 uneq12d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) } ∪ { 𝑏 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) } ) = ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( 𝑦 +s 𝑧 ) ) } ∪ { 𝑏 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( 𝑥 +s ( 𝑦𝐿 +s 𝑧 ) ) } ) )
70 oveq2 ⊢ ( 𝑧𝑂 = 𝑧𝐿 → ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝐿 ) )
71 oveq2 ⊢ ( 𝑧𝑂 = 𝑧𝐿 → ( 𝑦 +s 𝑧𝑂 ) = ( 𝑦 +s 𝑧𝐿 ) )
72 71 oveq2d ⊢ ( 𝑧𝑂 = 𝑧𝐿 → ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝐿 ) ) )
73 70 72 eqeq12d ⊢ ( 𝑧𝑂 = 𝑧𝐿 → ( ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ↔ ( ( 𝑥 +s 𝑦 ) +s 𝑧𝐿 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝐿 ) ) ) )
74 simplr3 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) → ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) )
75 elun1 ⊢ ( 𝑧𝐿 ∈ ( L ‘ 𝑧 ) → 𝑧𝐿 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
76 75 adantl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) → 𝑧𝐿 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
77 73 74 76 rspcdva ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) → ( ( 𝑥 +s 𝑦 ) +s 𝑧𝐿 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝐿 ) ) )
78 77 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) → ( 𝑐 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝐿 ) ↔ 𝑐 = ( 𝑥 +s ( 𝑦 +s 𝑧𝐿 ) ) ) )
79 78 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑐 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝐿 ) ↔ ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑐 = ( 𝑥 +s ( 𝑦 +s 𝑧𝐿 ) ) ) )
80 79 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → { 𝑐 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑐 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝐿 ) } = { 𝑐 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑐 = ( 𝑥 +s ( 𝑦 +s 𝑧𝐿 ) ) } )
81 69 80 uneq12d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) } ∪ { 𝑏 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) } ) ∪ { 𝑐 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑐 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝐿 ) } ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( 𝑦 +s 𝑧 ) ) } ∪ { 𝑏 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( 𝑥 +s ( 𝑦𝐿 +s 𝑧 ) ) } ) ∪ { 𝑐 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑐 = ( 𝑥 +s ( 𝑦 +s 𝑧𝐿 ) ) } ) )
82 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝑥𝑂 +s 𝑦 ) = ( 𝑥𝑅 +s 𝑦 ) )
83 82 oveq1d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( ( 𝑥𝑅 +s 𝑦 ) +s 𝑧 ) )
84 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) = ( 𝑥𝑅 +s ( 𝑦 +s 𝑧 ) ) )
85 83 84 eqeq12d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ↔ ( ( 𝑥𝑅 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑅 +s ( 𝑦 +s 𝑧 ) ) ) )
86 simplr1 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) )
87 elun2 ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
88 87 adantl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
89 85 86 88 rspcdva ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( ( 𝑥𝑅 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑅 +s ( 𝑦 +s 𝑧 ) ) )
90 89 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑑 = ( ( 𝑥𝑅 +s 𝑦 ) +s 𝑧 ) ↔ 𝑑 = ( 𝑥𝑅 +s ( 𝑦 +s 𝑧 ) ) ) )
91 90 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( ( 𝑥𝑅 +s 𝑦 ) +s 𝑧 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( 𝑥𝑅 +s ( 𝑦 +s 𝑧 ) ) ) )
92 91 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → { 𝑑 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( ( 𝑥𝑅 +s 𝑦 ) +s 𝑧 ) } = { 𝑑 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( 𝑥𝑅 +s ( 𝑦 +s 𝑧 ) ) } )
93 oveq2 ⊢ ( 𝑦𝑂 = 𝑦𝑅 → ( 𝑥 +s 𝑦𝑂 ) = ( 𝑥 +s 𝑦𝑅 ) )
94 93 oveq1d ⊢ ( 𝑦𝑂 = 𝑦𝑅 → ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( ( 𝑥 +s 𝑦𝑅 ) +s 𝑧 ) )
95 oveq1 ⊢ ( 𝑦𝑂 = 𝑦𝑅 → ( 𝑦𝑂 +s 𝑧 ) = ( 𝑦𝑅 +s 𝑧 ) )
96 95 oveq2d ⊢ ( 𝑦𝑂 = 𝑦𝑅 → ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) = ( 𝑥 +s ( 𝑦𝑅 +s 𝑧 ) ) )
97 94 96 eqeq12d ⊢ ( 𝑦𝑂 = 𝑦𝑅 → ( ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ↔ ( ( 𝑥 +s 𝑦𝑅 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑅 +s 𝑧 ) ) ) )
98 simplr2 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) )
99 elun2 ⊢ ( 𝑦𝑅 ∈ ( R ‘ 𝑦 ) → 𝑦𝑅 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
100 99 adantl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) → 𝑦𝑅 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
101 97 98 100 rspcdva ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) → ( ( 𝑥 +s 𝑦𝑅 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑅 +s 𝑧 ) ) )
102 101 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) → ( 𝑒 = ( ( 𝑥 +s 𝑦𝑅 ) +s 𝑧 ) ↔ 𝑒 = ( 𝑥 +s ( 𝑦𝑅 +s 𝑧 ) ) ) )
103 102 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( ( 𝑥 +s 𝑦𝑅 ) +s 𝑧 ) ↔ ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( 𝑥 +s ( 𝑦𝑅 +s 𝑧 ) ) ) )
104 103 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → { 𝑒 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( ( 𝑥 +s 𝑦𝑅 ) +s 𝑧 ) } = { 𝑒 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( 𝑥 +s ( 𝑦𝑅 +s 𝑧 ) ) } )
105 92 104 uneq12d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( { 𝑑 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( ( 𝑥𝑅 +s 𝑦 ) +s 𝑧 ) } ∪ { 𝑒 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( ( 𝑥 +s 𝑦𝑅 ) +s 𝑧 ) } ) = ( { 𝑑 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( 𝑥𝑅 +s ( 𝑦 +s 𝑧 ) ) } ∪ { 𝑒 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( 𝑥 +s ( 𝑦𝑅 +s 𝑧 ) ) } ) )
106 oveq2 ⊢ ( 𝑧𝑂 = 𝑧𝑅 → ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑅 ) )
107 oveq2 ⊢ ( 𝑧𝑂 = 𝑧𝑅 → ( 𝑦 +s 𝑧𝑂 ) = ( 𝑦 +s 𝑧𝑅 ) )
108 107 oveq2d ⊢ ( 𝑧𝑂 = 𝑧𝑅 → ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑅 ) ) )
109 106 108 eqeq12d ⊢ ( 𝑧𝑂 = 𝑧𝑅 → ( ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ↔ ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑅 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑅 ) ) ) )
110 simplr3 ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) → ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) )
111 elun2 ⊢ ( 𝑧𝑅 ∈ ( R ‘ 𝑧 ) → 𝑧𝑅 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
112 111 adantl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) → 𝑧𝑅 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
113 109 110 112 rspcdva ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) → ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑅 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑅 ) ) )
114 113 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) → ( 𝑓 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑅 ) ↔ 𝑓 = ( 𝑥 +s ( 𝑦 +s 𝑧𝑅 ) ) ) )
115 114 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑓 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑅 ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑓 = ( 𝑥 +s ( 𝑦 +s 𝑧𝑅 ) ) ) )
116 115 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → { 𝑓 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑓 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑅 ) } = { 𝑓 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑓 = ( 𝑥 +s ( 𝑦 +s 𝑧𝑅 ) ) } )
117 105 116 uneq12d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ( { 𝑑 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( ( 𝑥𝑅 +s 𝑦 ) +s 𝑧 ) } ∪ { 𝑒 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( ( 𝑥 +s 𝑦𝑅 ) +s 𝑧 ) } ) ∪ { 𝑓 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑓 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑅 ) } ) = ( ( { 𝑑 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( 𝑥𝑅 +s ( 𝑦 +s 𝑧 ) ) } ∪ { 𝑒 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( 𝑥 +s ( 𝑦𝑅 +s 𝑧 ) ) } ) ∪ { 𝑓 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑓 = ( 𝑥 +s ( 𝑦 +s 𝑧𝑅 ) ) } ) )
118 81 117 oveq12d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) } ∪ { 𝑏 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) } ) ∪ { 𝑐 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑐 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝐿 ) } ) |s ( ( { 𝑑 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( ( 𝑥𝑅 +s 𝑦 ) +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 𝑧𝑅 ) ) } ) ) )
119 simpl1 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → 𝑥 ∈ No )
120 simpl2 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → 𝑦 ∈ No )
121 simpl3 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → 𝑧 ∈ No )
122 119 120 121 addsasslem1 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ( 𝑥 +s 𝑦 ) +s 𝑧 ) = ( ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( ( 𝑥𝐿 +s 𝑦 ) +s 𝑧 ) } ∪ { 𝑏 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( ( 𝑥 +s 𝑦𝐿 ) +s 𝑧 ) } ) ∪ { 𝑐 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑐 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝐿 ) } ) |s ( ( { 𝑑 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( ( 𝑥𝑅 +s 𝑦 ) +s 𝑧 ) } ∪ { 𝑒 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( ( 𝑥 +s 𝑦𝑅 ) +s 𝑧 ) } ) ∪ { 𝑓 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑓 = ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑅 ) } ) ) )
123 119 120 121 addsasslem2 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( 𝑥 +s ( 𝑦 +s 𝑧 ) ) = ( ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑎 = ( 𝑥𝐿 +s ( 𝑦 +s 𝑧 ) ) } ∪ { 𝑏 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑏 = ( 𝑥 +s ( 𝑦𝐿 +s 𝑧 ) ) } ) ∪ { 𝑐 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑐 = ( 𝑥 +s ( 𝑦 +s 𝑧𝐿 ) ) } ) |s ( ( { 𝑑 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑑 = ( 𝑥𝑅 +s ( 𝑦 +s 𝑧 ) ) } ∪ { 𝑒 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑒 = ( 𝑥 +s ( 𝑦𝑅 +s 𝑧 ) ) } ) ∪ { 𝑓 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑓 = ( 𝑥 +s ( 𝑦 +s 𝑧𝑅 ) ) } ) ) )
124 118 122 123 3eqtr4d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ) → ( ( 𝑥 +s 𝑦 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦 +s 𝑧 ) ) )
125 124 ex ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) → ( ( 𝑥 +s 𝑦 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦 +s 𝑧 ) ) ) )
126 45 125 syl5 ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥𝑂 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦𝑂 +s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑥𝑂 +s 𝑦 ) +s 𝑧 ) = ( 𝑥𝑂 +s ( 𝑦 +s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 +s 𝑦𝑂 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦𝑂 +s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 +s 𝑦 ) +s 𝑧𝑂 ) = ( 𝑥 +s ( 𝑦 +s 𝑧𝑂 ) ) ) → ( ( 𝑥 +s 𝑦 ) +s 𝑧 ) = ( 𝑥 +s ( 𝑦 +s 𝑧 ) ) ) )
127 4 9 13 17 22 25 28 32 37 41 126 no3inds ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐴 +s 𝐵 ) +s 𝐶 ) = ( 𝐴 +s ( 𝐵 +s 𝐶 ) ) )