Step | Hyp | Ref
| Expression |
1 | | oveq1 7364 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑦) = (𝑥𝑂 +s 𝑦)) |
2 | | oveq2 7365 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑦 +s 𝑥) = (𝑦 +s 𝑥𝑂)) |
3 | 1, 2 | eqeq12d 2752 |
. 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 +s 𝑦) = (𝑦 +s 𝑥) ↔ (𝑥𝑂 +s 𝑦) = (𝑦 +s 𝑥𝑂))) |
4 | | oveq2 7365 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
+s 𝑦) = (𝑥𝑂
+s 𝑦𝑂)) |
5 | | oveq1 7364 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑥𝑂) = (𝑦𝑂
+s 𝑥𝑂)) |
6 | 4, 5 | eqeq12d 2752 |
. 2
⊢ (𝑦 = 𝑦𝑂 → ((𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ↔
(𝑥𝑂
+s 𝑦𝑂) = (𝑦𝑂 +s 𝑥𝑂))) |
7 | | oveq1 7364 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑦𝑂) = (𝑥𝑂
+s 𝑦𝑂)) |
8 | | oveq2 7365 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑦𝑂
+s 𝑥) = (𝑦𝑂
+s 𝑥𝑂)) |
9 | 7, 8 | eqeq12d 2752 |
. 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥) ↔
(𝑥𝑂
+s 𝑦𝑂) = (𝑦𝑂 +s 𝑥𝑂))) |
10 | | oveq1 7364 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 +s 𝑦) = (𝐴 +s 𝑦)) |
11 | | oveq2 7365 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑦 +s 𝑥) = (𝑦 +s 𝐴)) |
12 | 10, 11 | eqeq12d 2752 |
. 2
⊢ (𝑥 = 𝐴 → ((𝑥 +s 𝑦) = (𝑦 +s 𝑥) ↔ (𝐴 +s 𝑦) = (𝑦 +s 𝐴))) |
13 | | oveq2 7365 |
. . 3
⊢ (𝑦 = 𝐵 → (𝐴 +s 𝑦) = (𝐴 +s 𝐵)) |
14 | | oveq1 7364 |
. . 3
⊢ (𝑦 = 𝐵 → (𝑦 +s 𝐴) = (𝐵 +s 𝐴)) |
15 | 13, 14 | eqeq12d 2752 |
. 2
⊢ (𝑦 = 𝐵 → ((𝐴 +s 𝑦) = (𝑦 +s 𝐴) ↔ (𝐴 +s 𝐵) = (𝐵 +s 𝐴))) |
16 | | simpr2 1195 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂)) |
17 | | elun1 4136 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ ( L ‘𝑥) → 𝑙 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
18 | | oveq1 7364 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑙 → (𝑥𝑂 +s 𝑦) = (𝑙 +s 𝑦)) |
19 | | oveq2 7365 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑙 → (𝑦 +s 𝑥𝑂) = (𝑦 +s 𝑙)) |
20 | 18, 19 | eqeq12d 2752 |
. . . . . . . . . . . 12
⊢ (𝑥𝑂 = 𝑙 → ((𝑥𝑂 +s 𝑦) = (𝑦 +s 𝑥𝑂) ↔ (𝑙 +s 𝑦) = (𝑦 +s 𝑙))) |
21 | 20 | rspccva 3580 |
. . . . . . . . . . 11
⊢
((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 +s 𝑦) = (𝑦 +s 𝑥𝑂) ∧ 𝑙 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → (𝑙 +s 𝑦) = (𝑦 +s 𝑙)) |
22 | 16, 17, 21 | syl2an 596 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) ∧ 𝑙 ∈ ( L ‘𝑥)) → (𝑙 +s 𝑦) = (𝑦 +s 𝑙)) |
23 | 22 | eqeq2d 2747 |
. . . . . . . . 9
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) ∧ 𝑙 ∈ ( L ‘𝑥)) → (𝑤 = (𝑙 +s 𝑦) ↔ 𝑤 = (𝑦 +s 𝑙))) |
24 | 23 | rexbidva 3173 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → (∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑙 +s 𝑦) ↔ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙))) |
25 | 24 | abbidv 2805 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → {𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑙 +s 𝑦)} = {𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙)}) |
26 | | simpr3 1196 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥)) |
27 | | elun1 4136 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ ( L ‘𝑦) → 𝑙 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
28 | | oveq2 7365 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑙 → (𝑥 +s 𝑦𝑂) = (𝑥 +s 𝑙)) |
29 | | oveq1 7364 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑙 → (𝑦𝑂 +s 𝑥) = (𝑙 +s 𝑥)) |
30 | 28, 29 | eqeq12d 2752 |
. . . . . . . . . . . 12
⊢ (𝑦𝑂 = 𝑙 → ((𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥) ↔ (𝑥 +s 𝑙) = (𝑙 +s 𝑥))) |
31 | 30 | rspccva 3580 |
. . . . . . . . . . 11
⊢
((∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥) ∧ 𝑙 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) → (𝑥 +s 𝑙) = (𝑙 +s 𝑥)) |
32 | 26, 27, 31 | syl2an 596 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) ∧ 𝑙 ∈ ( L ‘𝑦)) → (𝑥 +s 𝑙) = (𝑙 +s 𝑥)) |
33 | 32 | eqeq2d 2747 |
. . . . . . . . 9
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) ∧ 𝑙 ∈ ( L ‘𝑦)) → (𝑧 = (𝑥 +s 𝑙) ↔ 𝑧 = (𝑙 +s 𝑥))) |
34 | 33 | rexbidva 3173 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → (∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑙) ↔ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥))) |
35 | 34 | abbidv 2805 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑙)} = {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥)}) |
36 | 25, 35 | uneq12d 4124 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → ({𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑙 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑙)}) = ({𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥)})) |
37 | | uncom 4113 |
. . . . . 6
⊢ ({𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥)}) = ({𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙)}) |
38 | 36, 37 | eqtrdi 2792 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → ({𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑙 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑙)}) = ({𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙)})) |
39 | | elun2 4137 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ( R ‘𝑥) → 𝑟 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
40 | | oveq1 7364 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑟 → (𝑥𝑂 +s 𝑦) = (𝑟 +s 𝑦)) |
41 | | oveq2 7365 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑂 = 𝑟 → (𝑦 +s 𝑥𝑂) = (𝑦 +s 𝑟)) |
42 | 40, 41 | eqeq12d 2752 |
. . . . . . . . . . . 12
⊢ (𝑥𝑂 = 𝑟 → ((𝑥𝑂 +s 𝑦) = (𝑦 +s 𝑥𝑂) ↔ (𝑟 +s 𝑦) = (𝑦 +s 𝑟))) |
43 | 42 | rspccva 3580 |
. . . . . . . . . . 11
⊢
((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 +s 𝑦) = (𝑦 +s 𝑥𝑂) ∧ 𝑟 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → (𝑟 +s 𝑦) = (𝑦 +s 𝑟)) |
44 | 16, 39, 43 | syl2an 596 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) ∧ 𝑟 ∈ ( R ‘𝑥)) → (𝑟 +s 𝑦) = (𝑦 +s 𝑟)) |
45 | 44 | eqeq2d 2747 |
. . . . . . . . 9
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) ∧ 𝑟 ∈ ( R ‘𝑥)) → (𝑤 = (𝑟 +s 𝑦) ↔ 𝑤 = (𝑦 +s 𝑟))) |
46 | 45 | rexbidva 3173 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → (∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑟 +s 𝑦) ↔ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟))) |
47 | 46 | abbidv 2805 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑟 +s 𝑦)} = {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟)}) |
48 | | elun2 4137 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ( R ‘𝑦) → 𝑟 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) |
49 | | oveq2 7365 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑟 → (𝑥 +s 𝑦𝑂) = (𝑥 +s 𝑟)) |
50 | | oveq1 7364 |
. . . . . . . . . . . . 13
⊢ (𝑦𝑂 = 𝑟 → (𝑦𝑂 +s 𝑥) = (𝑟 +s 𝑥)) |
51 | 49, 50 | eqeq12d 2752 |
. . . . . . . . . . . 12
⊢ (𝑦𝑂 = 𝑟 → ((𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥) ↔ (𝑥 +s 𝑟) = (𝑟 +s 𝑥))) |
52 | 51 | rspccva 3580 |
. . . . . . . . . . 11
⊢
((∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥) ∧ 𝑟 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))) → (𝑥 +s 𝑟) = (𝑟 +s 𝑥)) |
53 | 26, 48, 52 | syl2an 596 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) ∧ 𝑟 ∈ ( R ‘𝑦)) → (𝑥 +s 𝑟) = (𝑟 +s 𝑥)) |
54 | 53 | eqeq2d 2747 |
. . . . . . . . 9
⊢ ((((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) ∧ 𝑟 ∈ ( R ‘𝑦)) → (𝑧 = (𝑥 +s 𝑟) ↔ 𝑧 = (𝑟 +s 𝑥))) |
55 | 54 | rexbidva 3173 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → (∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑟) ↔ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥))) |
56 | 55 | abbidv 2805 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑟)} = {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥)}) |
57 | 47, 56 | uneq12d 4124 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑟 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑟)}) = ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥)})) |
58 | | uncom 4113 |
. . . . . 6
⊢ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥)}) = ({𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟)}) |
59 | 57, 58 | eqtrdi 2792 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑟 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑟)}) = ({𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟)})) |
60 | 38, 59 | oveq12d 7375 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → (({𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑙 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑙)}) |s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑟 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑟)})) = (({𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙)}) |s ({𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟)}))) |
61 | | addsval 27274 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → (𝑥 +s 𝑦) = (({𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑙 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑙)}) |s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑟 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑟)}))) |
62 | 61 | adantr 481 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → (𝑥 +s 𝑦) = (({𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑙 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑙)}) |s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑟 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑟)}))) |
63 | | addsval 27274 |
. . . . . 6
⊢ ((𝑦 ∈
No ∧ 𝑥 ∈
No ) → (𝑦 +s 𝑥) = (({𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙)}) |s ({𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟)}))) |
64 | 63 | ancoms 459 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → (𝑦 +s 𝑥) = (({𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙)}) |s ({𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟)}))) |
65 | 64 | adantr 481 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → (𝑦 +s 𝑥) = (({𝑧 ∣ ∃𝑙 ∈ ( L ‘𝑦)𝑧 = (𝑙 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑙 ∈ ( L ‘𝑥)𝑤 = (𝑦 +s 𝑙)}) |s ({𝑧 ∣ ∃𝑟 ∈ ( R ‘𝑦)𝑧 = (𝑟 +s 𝑥)} ∪ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑥)𝑤 = (𝑦 +s 𝑟)}))) |
66 | 60, 62, 65 | 3eqtr4d 2786 |
. . 3
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥))) → (𝑥 +s 𝑦) = (𝑦 +s 𝑥)) |
67 | 66 | ex 413 |
. 2
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥𝑂 +s 𝑦𝑂) = (𝑦𝑂
+s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
+s 𝑦) = (𝑦 +s 𝑥𝑂) ∧
∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))(𝑥 +s 𝑦𝑂) = (𝑦𝑂 +s 𝑥)) → (𝑥 +s 𝑦) = (𝑦 +s 𝑥))) |
68 | 3, 6, 9, 12, 15, 67 | no2inds 27267 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) |