Step | Hyp | Ref
| Expression |
1 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 +o 𝐵) = (𝐴 +o 𝐵)) |
2 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐵 +o 𝑥) = (𝐵 +o 𝐴)) |
3 | 1, 2 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 +o 𝐵) = (𝐵 +o 𝑥) ↔ (𝐴 +o 𝐵) = (𝐵 +o 𝐴))) |
4 | 3 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ ω → (𝑥 +o 𝐵) = (𝐵 +o 𝑥)) ↔ (𝐵 ∈ ω → (𝐴 +o 𝐵) = (𝐵 +o 𝐴)))) |
5 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = ∅ → (𝑥 +o 𝐵) = (∅ +o 𝐵)) |
6 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐵 +o 𝑥) = (𝐵 +o ∅)) |
7 | 5, 6 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = ∅ → ((𝑥 +o 𝐵) = (𝐵 +o 𝑥) ↔ (∅ +o 𝐵) = (𝐵 +o ∅))) |
8 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 +o 𝐵) = (𝑦 +o 𝐵)) |
9 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o 𝑦)) |
10 | 8, 9 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 +o 𝐵) = (𝐵 +o 𝑥) ↔ (𝑦 +o 𝐵) = (𝐵 +o 𝑦))) |
11 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝑥 +o 𝐵) = (suc 𝑦 +o 𝐵)) |
12 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o suc 𝑦)) |
13 | 11, 12 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝑥 +o 𝐵) = (𝐵 +o 𝑥) ↔ (suc 𝑦 +o 𝐵) = (𝐵 +o suc 𝑦))) |
14 | | nna0r 8337 |
. . . . 5
⊢ (𝐵 ∈ ω → (∅
+o 𝐵) = 𝐵) |
15 | | nna0 8332 |
. . . . 5
⊢ (𝐵 ∈ ω → (𝐵 +o ∅) = 𝐵) |
16 | 14, 15 | eqtr4d 2780 |
. . . 4
⊢ (𝐵 ∈ ω → (∅
+o 𝐵) = (𝐵 +o
∅)) |
17 | | suceq 6278 |
. . . . . 6
⊢ ((𝑦 +o 𝐵) = (𝐵 +o 𝑦) → suc (𝑦 +o 𝐵) = suc (𝐵 +o 𝑦)) |
18 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → (suc 𝑦 +o 𝑥) = (suc 𝑦 +o 𝐵)) |
19 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (𝑦 +o 𝑥) = (𝑦 +o 𝐵)) |
20 | | suceq 6278 |
. . . . . . . . . . . 12
⊢ ((𝑦 +o 𝑥) = (𝑦 +o 𝐵) → suc (𝑦 +o 𝑥) = suc (𝑦 +o 𝐵)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → suc (𝑦 +o 𝑥) = suc (𝑦 +o 𝐵)) |
22 | 18, 21 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ((suc 𝑦 +o 𝑥) = suc (𝑦 +o 𝑥) ↔ (suc 𝑦 +o 𝐵) = suc (𝑦 +o 𝐵))) |
23 | 22 | imbi2d 344 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝑦 ∈ ω → (suc 𝑦 +o 𝑥) = suc (𝑦 +o 𝑥)) ↔ (𝑦 ∈ ω → (suc 𝑦 +o 𝐵) = suc (𝑦 +o 𝐵)))) |
24 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (suc 𝑦 +o 𝑥) = (suc 𝑦 +o ∅)) |
25 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑦 +o 𝑥) = (𝑦 +o ∅)) |
26 | | suceq 6278 |
. . . . . . . . . . . 12
⊢ ((𝑦 +o 𝑥) = (𝑦 +o ∅) → suc (𝑦 +o 𝑥) = suc (𝑦 +o ∅)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → suc (𝑦 +o 𝑥) = suc (𝑦 +o ∅)) |
28 | 24, 27 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((suc 𝑦 +o 𝑥) = suc (𝑦 +o 𝑥) ↔ (suc 𝑦 +o ∅) = suc (𝑦 +o
∅))) |
29 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (suc 𝑦 +o 𝑥) = (suc 𝑦 +o 𝑧)) |
30 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑦 +o 𝑥) = (𝑦 +o 𝑧)) |
31 | | suceq 6278 |
. . . . . . . . . . . 12
⊢ ((𝑦 +o 𝑥) = (𝑦 +o 𝑧) → suc (𝑦 +o 𝑥) = suc (𝑦 +o 𝑧)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → suc (𝑦 +o 𝑥) = suc (𝑦 +o 𝑧)) |
33 | 29, 32 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((suc 𝑦 +o 𝑥) = suc (𝑦 +o 𝑥) ↔ (suc 𝑦 +o 𝑧) = suc (𝑦 +o 𝑧))) |
34 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑧 → (suc 𝑦 +o 𝑥) = (suc 𝑦 +o suc 𝑧)) |
35 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢ (𝑥 = suc 𝑧 → (𝑦 +o 𝑥) = (𝑦 +o suc 𝑧)) |
36 | | suceq 6278 |
. . . . . . . . . . . 12
⊢ ((𝑦 +o 𝑥) = (𝑦 +o suc 𝑧) → suc (𝑦 +o 𝑥) = suc (𝑦 +o suc 𝑧)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑧 → suc (𝑦 +o 𝑥) = suc (𝑦 +o suc 𝑧)) |
38 | 34, 37 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑧 → ((suc 𝑦 +o 𝑥) = suc (𝑦 +o 𝑥) ↔ (suc 𝑦 +o suc 𝑧) = suc (𝑦 +o suc 𝑧))) |
39 | | peano2 7668 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) |
40 | | nna0 8332 |
. . . . . . . . . . . 12
⊢ (suc
𝑦 ∈ ω →
(suc 𝑦 +o
∅) = suc 𝑦) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω → (suc
𝑦 +o ∅) =
suc 𝑦) |
42 | | nna0 8332 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω → (𝑦 +o ∅) = 𝑦) |
43 | | suceq 6278 |
. . . . . . . . . . . 12
⊢ ((𝑦 +o ∅) = 𝑦 → suc (𝑦 +o ∅) = suc 𝑦) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω → suc
(𝑦 +o ∅) =
suc 𝑦) |
45 | 41, 44 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω → (suc
𝑦 +o ∅) =
suc (𝑦 +o
∅)) |
46 | | suceq 6278 |
. . . . . . . . . . . 12
⊢ ((suc
𝑦 +o 𝑧) = suc (𝑦 +o 𝑧) → suc (suc 𝑦 +o 𝑧) = suc suc (𝑦 +o 𝑧)) |
47 | | nnasuc 8334 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑦 ∈ ω ∧
𝑧 ∈ ω) →
(suc 𝑦 +o suc
𝑧) = suc (suc 𝑦 +o 𝑧)) |
48 | 39, 47 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (suc
𝑦 +o suc 𝑧) = suc (suc 𝑦 +o 𝑧)) |
49 | | nnasuc 8334 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (𝑦 +o suc 𝑧) = suc (𝑦 +o 𝑧)) |
50 | | suceq 6278 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 +o suc 𝑧) = suc (𝑦 +o 𝑧) → suc (𝑦 +o suc 𝑧) = suc suc (𝑦 +o 𝑧)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → suc
(𝑦 +o suc 𝑧) = suc suc (𝑦 +o 𝑧)) |
52 | 48, 51 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → ((suc
𝑦 +o suc 𝑧) = suc (𝑦 +o suc 𝑧) ↔ suc (suc 𝑦 +o 𝑧) = suc suc (𝑦 +o 𝑧))) |
53 | 46, 52 | syl5ibr 249 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → ((suc
𝑦 +o 𝑧) = suc (𝑦 +o 𝑧) → (suc 𝑦 +o suc 𝑧) = suc (𝑦 +o suc 𝑧))) |
54 | 53 | expcom 417 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ω → (𝑦 ∈ ω → ((suc
𝑦 +o 𝑧) = suc (𝑦 +o 𝑧) → (suc 𝑦 +o suc 𝑧) = suc (𝑦 +o suc 𝑧)))) |
55 | 28, 33, 38, 45, 54 | finds2 7678 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → (𝑦 ∈ ω → (suc
𝑦 +o 𝑥) = suc (𝑦 +o 𝑥))) |
56 | 23, 55 | vtoclga 3489 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → (𝑦 ∈ ω → (suc
𝑦 +o 𝐵) = suc (𝑦 +o 𝐵))) |
57 | 56 | imp 410 |
. . . . . . 7
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝑦 +o 𝐵) = suc (𝑦 +o 𝐵)) |
58 | | nnasuc 8334 |
. . . . . . 7
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 +o suc 𝑦) = suc (𝐵 +o 𝑦)) |
59 | 57, 58 | eqeq12d 2753 |
. . . . . 6
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → ((suc
𝑦 +o 𝐵) = (𝐵 +o suc 𝑦) ↔ suc (𝑦 +o 𝐵) = suc (𝐵 +o 𝑦))) |
60 | 17, 59 | syl5ibr 249 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → ((𝑦 +o 𝐵) = (𝐵 +o 𝑦) → (suc 𝑦 +o 𝐵) = (𝐵 +o suc 𝑦))) |
61 | 60 | expcom 417 |
. . . 4
⊢ (𝑦 ∈ ω → (𝐵 ∈ ω → ((𝑦 +o 𝐵) = (𝐵 +o 𝑦) → (suc 𝑦 +o 𝐵) = (𝐵 +o suc 𝑦)))) |
62 | 7, 10, 13, 16, 61 | finds2 7678 |
. . 3
⊢ (𝑥 ∈ ω → (𝐵 ∈ ω → (𝑥 +o 𝐵) = (𝐵 +o 𝑥))) |
63 | 4, 62 | vtoclga 3489 |
. 2
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐴 +o 𝐵) = (𝐵 +o 𝐴))) |
64 | 63 | imp 410 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) = (𝐵 +o 𝐴)) |