| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq1 7439 | . . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑦) = (𝑥𝑂 +s 𝑦)) | 
| 2 | 1 | oveq1d 7447 | . . 3
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 +s 𝑦) +s 𝑧) = ((𝑥𝑂 +s 𝑦) +s 𝑧)) | 
| 3 |  | oveq1 7439 | . . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 +s (𝑦 +s 𝑧)) = (𝑥𝑂 +s (𝑦 +s 𝑧))) | 
| 4 | 2, 3 | eqeq12d 2752 | . 2
⊢ (𝑥 = 𝑥𝑂 → (((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧)) ↔ ((𝑥𝑂 +s 𝑦) +s 𝑧) = (𝑥𝑂 +s (𝑦 +s 𝑧)))) | 
| 5 |  | oveq2 7440 | . . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
+s 𝑦) = (𝑥𝑂
+s 𝑦𝑂)) | 
| 6 | 5 | oveq1d 7447 | . . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
+s 𝑦)
+s 𝑧) = ((𝑥𝑂
+s 𝑦𝑂) +s 𝑧)) | 
| 7 |  | oveq1 7439 | . . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧) = (𝑦𝑂 +s 𝑧)) | 
| 8 | 7 | oveq2d 7448 | . . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
+s (𝑦
+s 𝑧)) = (𝑥𝑂
+s (𝑦𝑂 +s 𝑧))) | 
| 9 | 6, 8 | eqeq12d 2752 | . 2
⊢ (𝑦 = 𝑦𝑂 → (((𝑥𝑂
+s 𝑦)
+s 𝑧) = (𝑥𝑂
+s (𝑦
+s 𝑧)) ↔
((𝑥𝑂
+s 𝑦𝑂) +s 𝑧) = (𝑥𝑂 +s (𝑦𝑂
+s 𝑧)))) | 
| 10 |  | oveq2 7440 | . . 3
⊢ (𝑧 = 𝑧𝑂 → ((𝑥𝑂
+s 𝑦𝑂) +s 𝑧) = ((𝑥𝑂 +s 𝑦𝑂)
+s 𝑧𝑂)) | 
| 11 |  | oveq2 7440 | . . . 4
⊢ (𝑧 = 𝑧𝑂 → (𝑦𝑂
+s 𝑧) = (𝑦𝑂
+s 𝑧𝑂)) | 
| 12 | 11 | oveq2d 7448 | . . 3
⊢ (𝑧 = 𝑧𝑂 → (𝑥𝑂
+s (𝑦𝑂 +s 𝑧)) = (𝑥𝑂 +s (𝑦𝑂
+s 𝑧𝑂))) | 
| 13 | 10, 12 | eqeq12d 2752 | . 2
⊢ (𝑧 = 𝑧𝑂 → (((𝑥𝑂
+s 𝑦𝑂) +s 𝑧) = (𝑥𝑂 +s (𝑦𝑂
+s 𝑧)) ↔
((𝑥𝑂
+s 𝑦𝑂) +s 𝑧𝑂) = (𝑥𝑂
+s (𝑦𝑂 +s 𝑧𝑂)))) | 
| 14 |  | oveq1 7439 | . . . 4
⊢ (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑦𝑂) = (𝑥𝑂
+s 𝑦𝑂)) | 
| 15 | 14 | oveq1d 7447 | . . 3
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 +s 𝑦𝑂)
+s 𝑧𝑂) = ((𝑥𝑂 +s 𝑦𝑂)
+s 𝑧𝑂)) | 
| 16 |  | oveq1 7439 | . . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 +s (𝑦𝑂
+s 𝑧𝑂)) = (𝑥𝑂 +s (𝑦𝑂
+s 𝑧𝑂))) | 
| 17 | 15, 16 | eqeq12d 2752 | . 2
⊢ (𝑥 = 𝑥𝑂 → (((𝑥 +s 𝑦𝑂)
+s 𝑧𝑂) = (𝑥 +s (𝑦𝑂 +s 𝑧𝑂)) ↔
((𝑥𝑂
+s 𝑦𝑂) +s 𝑧𝑂) = (𝑥𝑂
+s (𝑦𝑂 +s 𝑧𝑂)))) | 
| 18 |  | oveq2 7440 | . . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑥 +s 𝑦) = (𝑥 +s 𝑦𝑂)) | 
| 19 | 18 | oveq1d 7447 | . . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥 +s 𝑦) +s 𝑧𝑂) = ((𝑥 +s 𝑦𝑂)
+s 𝑧𝑂)) | 
| 20 |  | oveq1 7439 | . . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧𝑂) = (𝑦𝑂
+s 𝑧𝑂)) | 
| 21 | 20 | oveq2d 7448 | . . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥 +s (𝑦 +s 𝑧𝑂)) = (𝑥 +s (𝑦𝑂
+s 𝑧𝑂))) | 
| 22 | 19, 21 | eqeq12d 2752 | . 2
⊢ (𝑦 = 𝑦𝑂 → (((𝑥 +s 𝑦) +s 𝑧𝑂) = (𝑥 +s (𝑦 +s 𝑧𝑂)) ↔
((𝑥 +s 𝑦𝑂)
+s 𝑧𝑂) = (𝑥 +s (𝑦𝑂 +s 𝑧𝑂)))) | 
| 23 | 5 | oveq1d 7447 | . . 3
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
+s 𝑦)
+s 𝑧𝑂) = ((𝑥𝑂 +s 𝑦𝑂)
+s 𝑧𝑂)) | 
| 24 | 20 | oveq2d 7448 | . . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
+s (𝑦
+s 𝑧𝑂)) = (𝑥𝑂 +s (𝑦𝑂
+s 𝑧𝑂))) | 
| 25 | 23, 24 | eqeq12d 2752 | . 2
⊢ (𝑦 = 𝑦𝑂 → (((𝑥𝑂
+s 𝑦)
+s 𝑧𝑂) = (𝑥𝑂 +s (𝑦 +s 𝑧𝑂)) ↔
((𝑥𝑂
+s 𝑦𝑂) +s 𝑧𝑂) = (𝑥𝑂
+s (𝑦𝑂 +s 𝑧𝑂)))) | 
| 26 |  | oveq2 7440 | . . 3
⊢ (𝑧 = 𝑧𝑂 → ((𝑥 +s 𝑦𝑂)
+s 𝑧) = ((𝑥 +s 𝑦𝑂)
+s 𝑧𝑂)) | 
| 27 | 11 | oveq2d 7448 | . . 3
⊢ (𝑧 = 𝑧𝑂 → (𝑥 +s (𝑦𝑂
+s 𝑧)) = (𝑥 +s (𝑦𝑂
+s 𝑧𝑂))) | 
| 28 | 26, 27 | eqeq12d 2752 | . 2
⊢ (𝑧 = 𝑧𝑂 → (((𝑥 +s 𝑦𝑂)
+s 𝑧) = (𝑥 +s (𝑦𝑂
+s 𝑧)) ↔
((𝑥 +s 𝑦𝑂)
+s 𝑧𝑂) = (𝑥 +s (𝑦𝑂 +s 𝑧𝑂)))) | 
| 29 |  | oveq1 7439 | . . . 4
⊢ (𝑥 = 𝐴 → (𝑥 +s 𝑦) = (𝐴 +s 𝑦)) | 
| 30 | 29 | oveq1d 7447 | . . 3
⊢ (𝑥 = 𝐴 → ((𝑥 +s 𝑦) +s 𝑧) = ((𝐴 +s 𝑦) +s 𝑧)) | 
| 31 |  | oveq1 7439 | . . 3
⊢ (𝑥 = 𝐴 → (𝑥 +s (𝑦 +s 𝑧)) = (𝐴 +s (𝑦 +s 𝑧))) | 
| 32 | 30, 31 | eqeq12d 2752 | . 2
⊢ (𝑥 = 𝐴 → (((𝑥 +s 𝑦) +s 𝑧) = (𝑥 +s (𝑦 +s 𝑧)) ↔ ((𝐴 +s 𝑦) +s 𝑧) = (𝐴 +s (𝑦 +s 𝑧)))) | 
| 33 |  | oveq2 7440 | . . . 4
⊢ (𝑦 = 𝐵 → (𝐴 +s 𝑦) = (𝐴 +s 𝐵)) | 
| 34 | 33 | oveq1d 7447 | . . 3
⊢ (𝑦 = 𝐵 → ((𝐴 +s 𝑦) +s 𝑧) = ((𝐴 +s 𝐵) +s 𝑧)) | 
| 35 |  | oveq1 7439 | . . . 4
⊢ (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧)) | 
| 36 | 35 | oveq2d 7448 | . . 3
⊢ (𝑦 = 𝐵 → (𝐴 +s (𝑦 +s 𝑧)) = (𝐴 +s (𝐵 +s 𝑧))) | 
| 37 | 34, 36 | eqeq12d 2752 | . 2
⊢ (𝑦 = 𝐵 → (((𝐴 +s 𝑦) +s 𝑧) = (𝐴 +s (𝑦 +s 𝑧)) ↔ ((𝐴 +s 𝐵) +s 𝑧) = (𝐴 +s (𝐵 +s 𝑧)))) | 
| 38 |  | oveq2 7440 | . . 3
⊢ (𝑧 = 𝐶 → ((𝐴 +s 𝐵) +s 𝑧) = ((𝐴 +s 𝐵) +s 𝐶)) | 
| 39 |  | oveq2 7440 | . . . 4
⊢ (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶)) | 
| 40 | 39 | oveq2d 7448 | . . 3
⊢ (𝑧 = 𝐶 → (𝐴 +s (𝐵 +s 𝑧)) = (𝐴 +s (𝐵 +s 𝐶))) | 
| 41 | 38, 40 | eqeq12d 2752 | . 2
⊢ (𝑧 = 𝐶 → (((𝐴 +s 𝐵) +s 𝑧) = (𝐴 +s (𝐵 +s 𝑧)) ↔ ((𝐴 +s 𝐵) +s 𝐶) = (𝐴 +s (𝐵 +s 𝐶)))) | 
| 42 |  | simp21 1206 | . . . 4
⊢
(((∀𝑥𝑂 ∈ (( 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 1208 | . . . 4
⊢
(((∀𝑥𝑂 ∈ (( 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 1138 | . . . 4
⊢
(((∀𝑥𝑂 ∈ (( 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 1128 | . . 3
⊢
(((∀𝑥𝑂 ∈ (( 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 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥𝑂 = 𝑥𝐿 →
(𝑥𝑂
+s 𝑦) = (𝑥𝐿
+s 𝑦)) | 
| 47 | 46 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑥𝐿 →
((𝑥𝑂
+s 𝑦)
+s 𝑧) = ((𝑥𝐿
+s 𝑦)
+s 𝑧)) | 
| 48 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑥𝐿 →
(𝑥𝑂
+s (𝑦
+s 𝑧)) = (𝑥𝐿
+s (𝑦
+s 𝑧))) | 
| 49 | 47, 48 | eqeq12d 2752 | . . . . . . . . . . . 12
⊢ (𝑥𝑂 = 𝑥𝐿 →
(((𝑥𝑂
+s 𝑦)
+s 𝑧) = (𝑥𝑂
+s (𝑦
+s 𝑧)) ↔
((𝑥𝐿
+s 𝑦)
+s 𝑧) = (𝑥𝐿
+s (𝑦
+s 𝑧)))) | 
| 50 |  | simplr1 1215 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 
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 4181 | . . . . . . . . . . . . 13
⊢ (𝑥𝐿 ∈ ( L
‘𝑥) → 𝑥𝐿 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 52 | 51 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 
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 3622 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
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 2747 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
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 3176 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
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 2807 | . . . . . . . 8
⊢ (((𝑥 ∈ 
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 7440 | . . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑦𝐿 →
(𝑥 +s 𝑦𝑂) = (𝑥 +s 𝑦𝐿)) | 
| 58 | 57 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑦𝐿 →
((𝑥 +s 𝑦𝑂)
+s 𝑧) = ((𝑥 +s 𝑦𝐿)
+s 𝑧)) | 
| 59 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑦𝐿 →
(𝑦𝑂
+s 𝑧) = (𝑦𝐿
+s 𝑧)) | 
| 60 | 59 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑦𝐿 →
(𝑥 +s (𝑦𝑂
+s 𝑧)) = (𝑥 +s (𝑦𝐿
+s 𝑧))) | 
| 61 | 58, 60 | eqeq12d 2752 | . . . . . . . . . . . 12
⊢ (𝑦𝑂 = 𝑦𝐿 →
(((𝑥 +s 𝑦𝑂)
+s 𝑧) = (𝑥 +s (𝑦𝑂
+s 𝑧)) ↔
((𝑥 +s 𝑦𝐿)
+s 𝑧) = (𝑥 +s (𝑦𝐿
+s 𝑧)))) | 
| 62 |  | simplr2 1216 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 
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 4181 | . . . . . . . . . . . . 13
⊢ (𝑦𝐿 ∈ ( L
‘𝑦) → 𝑦𝐿 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) | 
| 64 | 63 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 
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 3622 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
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 2747 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
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 3176 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
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 2807 | . . . . . . . 8
⊢ (((𝑥 ∈ 
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 4168 | . . . . . . 7
⊢ (((𝑥 ∈ 
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 7440 | . . . . . . . . . . . 12
⊢ (𝑧𝑂 = 𝑧𝐿 →
((𝑥 +s 𝑦) +s 𝑧𝑂) = ((𝑥 +s 𝑦) +s 𝑧𝐿)) | 
| 71 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑧𝑂 = 𝑧𝐿 →
(𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝐿)) | 
| 72 | 71 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑧𝑂 = 𝑧𝐿 →
(𝑥 +s (𝑦 +s 𝑧𝑂)) = (𝑥 +s (𝑦 +s 𝑧𝐿))) | 
| 73 | 70, 72 | eqeq12d 2752 | . . . . . . . . . . 11
⊢ (𝑧𝑂 = 𝑧𝐿 →
(((𝑥 +s 𝑦) +s 𝑧𝑂) = (𝑥 +s (𝑦 +s 𝑧𝑂)) ↔
((𝑥 +s 𝑦) +s 𝑧𝐿) = (𝑥 +s (𝑦 +s 𝑧𝐿)))) | 
| 74 |  | simplr3 1217 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
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 4181 | . . . . . . . . . . . 12
⊢ (𝑧𝐿 ∈ ( L
‘𝑧) → 𝑧𝐿 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) | 
| 76 | 75 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
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 3622 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
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 2747 | . . . . . . . . 9
⊢ ((((𝑥 ∈ 
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 3176 | . . . . . . . 8
⊢ (((𝑥 ∈ 
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 2807 | . . . . . . 7
⊢ (((𝑥 ∈ 
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 4168 | . . . . . 6
⊢ (((𝑥 ∈ 
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 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥𝑂 = 𝑥𝑅 →
(𝑥𝑂
+s 𝑦) = (𝑥𝑅
+s 𝑦)) | 
| 83 | 82 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑥𝑅 →
((𝑥𝑂
+s 𝑦)
+s 𝑧) = ((𝑥𝑅
+s 𝑦)
+s 𝑧)) | 
| 84 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑥𝑅 →
(𝑥𝑂
+s (𝑦
+s 𝑧)) = (𝑥𝑅
+s (𝑦
+s 𝑧))) | 
| 85 | 83, 84 | eqeq12d 2752 | . . . . . . . . . . . 12
⊢ (𝑥𝑂 = 𝑥𝑅 →
(((𝑥𝑂
+s 𝑦)
+s 𝑧) = (𝑥𝑂
+s (𝑦
+s 𝑧)) ↔
((𝑥𝑅
+s 𝑦)
+s 𝑧) = (𝑥𝑅
+s (𝑦
+s 𝑧)))) | 
| 86 |  | simplr1 1215 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 
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 4182 | . . . . . . . . . . . . 13
⊢ (𝑥𝑅 ∈ ( R
‘𝑥) → 𝑥𝑅 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))) | 
| 88 | 87 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 
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 3622 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
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 2747 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
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 3176 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
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 2807 | . . . . . . . 8
⊢ (((𝑥 ∈ 
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 7440 | . . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑦𝑅 →
(𝑥 +s 𝑦𝑂) = (𝑥 +s 𝑦𝑅)) | 
| 94 | 93 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑦𝑅 →
((𝑥 +s 𝑦𝑂)
+s 𝑧) = ((𝑥 +s 𝑦𝑅)
+s 𝑧)) | 
| 95 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑦𝑂 = 𝑦𝑅 →
(𝑦𝑂
+s 𝑧) = (𝑦𝑅
+s 𝑧)) | 
| 96 | 95 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑦𝑅 →
(𝑥 +s (𝑦𝑂
+s 𝑧)) = (𝑥 +s (𝑦𝑅
+s 𝑧))) | 
| 97 | 94, 96 | eqeq12d 2752 | . . . . . . . . . . . 12
⊢ (𝑦𝑂 = 𝑦𝑅 →
(((𝑥 +s 𝑦𝑂)
+s 𝑧) = (𝑥 +s (𝑦𝑂
+s 𝑧)) ↔
((𝑥 +s 𝑦𝑅)
+s 𝑧) = (𝑥 +s (𝑦𝑅
+s 𝑧)))) | 
| 98 |  | simplr2 1216 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 
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 4182 | . . . . . . . . . . . . 13
⊢ (𝑦𝑅 ∈ ( R
‘𝑦) → 𝑦𝑅 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))) | 
| 100 | 99 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 
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 3622 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
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 2747 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
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 3176 | . . . . . . . . 9
⊢ (((𝑥 ∈ 
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 2807 | . . . . . . . 8
⊢ (((𝑥 ∈ 
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 4168 | . . . . . . 7
⊢ (((𝑥 ∈ 
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 7440 | . . . . . . . . . . . 12
⊢ (𝑧𝑂 = 𝑧𝑅 →
((𝑥 +s 𝑦) +s 𝑧𝑂) = ((𝑥 +s 𝑦) +s 𝑧𝑅)) | 
| 107 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑧𝑂 = 𝑧𝑅 →
(𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝑅)) | 
| 108 | 107 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑧𝑂 = 𝑧𝑅 →
(𝑥 +s (𝑦 +s 𝑧𝑂)) = (𝑥 +s (𝑦 +s 𝑧𝑅))) | 
| 109 | 106, 108 | eqeq12d 2752 | . . . . . . . . . . 11
⊢ (𝑧𝑂 = 𝑧𝑅 →
(((𝑥 +s 𝑦) +s 𝑧𝑂) = (𝑥 +s (𝑦 +s 𝑧𝑂)) ↔
((𝑥 +s 𝑦) +s 𝑧𝑅) = (𝑥 +s (𝑦 +s 𝑧𝑅)))) | 
| 110 |  | simplr3 1217 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
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 4182 | . . . . . . . . . . . 12
⊢ (𝑧𝑅 ∈ ( R
‘𝑧) → 𝑧𝑅 ∈ (( L
‘𝑧) ∪ ( R
‘𝑧))) | 
| 112 | 111 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ 
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 3622 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ 
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 2747 | . . . . . . . . 9
⊢ ((((𝑥 ∈ 
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 3176 | . . . . . . . 8
⊢ (((𝑥 ∈ 
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 2807 | . . . . . . 7
⊢ (((𝑥 ∈ 
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 4168 | . . . . . 6
⊢ (((𝑥 ∈ 
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 7450 | . . . . 5
⊢ (((𝑥 ∈ 
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 1191 | . . . . . 6
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥𝑂 +s 𝑦) +s 𝑧) = (𝑥𝑂 +s (𝑦 +s 𝑧)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦𝑂)
+s 𝑧) = (𝑥 +s (𝑦𝑂
+s 𝑧)) ∧
∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧𝑂) = (𝑥 +s (𝑦 +s 𝑧𝑂)))) → 𝑥 ∈ 
No ) | 
| 120 |  | simpl2 1192 | . . . . . 6
⊢ (((𝑥 ∈ 
No  ∧ 𝑦 ∈
 No  ∧ 𝑧 ∈  No )
∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑥𝑂 +s 𝑦) +s 𝑧) = (𝑥𝑂 +s (𝑦 +s 𝑧)) ∧ ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))((𝑥 +s 𝑦𝑂)
+s 𝑧) = (𝑥 +s (𝑦𝑂
+s 𝑧)) ∧
∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑥 +s 𝑦) +s 𝑧𝑂) = (𝑥 +s (𝑦 +s 𝑧𝑂)))) → 𝑦 ∈ 
No ) | 
| 121 |  | simpl3 1193 | . . . . . 6
⊢ (((𝑥 ∈ 
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 28037 | . . . . 5
⊢ (((𝑥 ∈ 
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 28038 | . . . . 5
⊢ (((𝑥 ∈ 
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 2786 | . . . 4
⊢ (((𝑥 ∈ 
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 412 | . . 3
⊢ ((𝑥 ∈ 
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 34 | . 2
⊢ ((𝑥 ∈ 
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 27992 | 1
⊢ ((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No  ∧ 𝐶 ∈  No )
→ ((𝐴 +s
𝐵) +s 𝐶) = (𝐴 +s (𝐵 +s 𝐶))) |