| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . 6
⊢ (𝑛 = 1 → (𝑛 + 1) = (1 + 1)) |
| 2 | 1 | oveq2d 7447 |
. . . . 5
⊢ (𝑛 = 1 → (𝑅↑𝑟(𝑛 + 1)) = (𝑅↑𝑟(1 +
1))) |
| 3 | | oveq2 7439 |
. . . . . 6
⊢ (𝑛 = 1 → (𝑅↑𝑟𝑛) = (𝑅↑𝑟1)) |
| 4 | 3 | coeq2d 5873 |
. . . . 5
⊢ (𝑛 = 1 → (𝑅 ∘ (𝑅↑𝑟𝑛)) = (𝑅 ∘ (𝑅↑𝑟1))) |
| 5 | 2, 4 | eqeq12d 2753 |
. . . 4
⊢ (𝑛 = 1 → ((𝑅↑𝑟(𝑛 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑛)) ↔ (𝑅↑𝑟(1 + 1)) = (𝑅 ∘ (𝑅↑𝑟1)))) |
| 6 | 5 | imbi2d 340 |
. . 3
⊢ (𝑛 = 1 → ((𝑅 ∈ 𝑉 → (𝑅↑𝑟(𝑛 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑛))) ↔ (𝑅 ∈ 𝑉 → (𝑅↑𝑟(1 + 1)) = (𝑅 ∘ (𝑅↑𝑟1))))) |
| 7 | | oveq1 7438 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑛 + 1) = (𝑚 + 1)) |
| 8 | 7 | oveq2d 7447 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝑅↑𝑟(𝑛 + 1)) = (𝑅↑𝑟(𝑚 + 1))) |
| 9 | | oveq2 7439 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑅↑𝑟𝑛) = (𝑅↑𝑟𝑚)) |
| 10 | 9 | coeq2d 5873 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝑅 ∘ (𝑅↑𝑟𝑛)) = (𝑅 ∘ (𝑅↑𝑟𝑚))) |
| 11 | 8, 10 | eqeq12d 2753 |
. . . 4
⊢ (𝑛 = 𝑚 → ((𝑅↑𝑟(𝑛 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑛)) ↔ (𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚)))) |
| 12 | 11 | imbi2d 340 |
. . 3
⊢ (𝑛 = 𝑚 → ((𝑅 ∈ 𝑉 → (𝑅↑𝑟(𝑛 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑛))) ↔ (𝑅 ∈ 𝑉 → (𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚))))) |
| 13 | | oveq1 7438 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝑛 + 1) = ((𝑚 + 1) + 1)) |
| 14 | 13 | oveq2d 7447 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (𝑅↑𝑟(𝑛 + 1)) = (𝑅↑𝑟((𝑚 + 1) + 1))) |
| 15 | | oveq2 7439 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝑅↑𝑟𝑛) = (𝑅↑𝑟(𝑚 + 1))) |
| 16 | 15 | coeq2d 5873 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (𝑅 ∘ (𝑅↑𝑟𝑛)) = (𝑅 ∘ (𝑅↑𝑟(𝑚 + 1)))) |
| 17 | 14, 16 | eqeq12d 2753 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → ((𝑅↑𝑟(𝑛 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑛)) ↔ (𝑅↑𝑟((𝑚 + 1) + 1)) = (𝑅 ∘ (𝑅↑𝑟(𝑚 + 1))))) |
| 18 | 17 | imbi2d 340 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → ((𝑅 ∈ 𝑉 → (𝑅↑𝑟(𝑛 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑛))) ↔ (𝑅 ∈ 𝑉 → (𝑅↑𝑟((𝑚 + 1) + 1)) = (𝑅 ∘ (𝑅↑𝑟(𝑚 + 1)))))) |
| 19 | | oveq1 7438 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 + 1) = (𝑁 + 1)) |
| 20 | 19 | oveq2d 7447 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑅↑𝑟(𝑛 + 1)) = (𝑅↑𝑟(𝑁 + 1))) |
| 21 | | oveq2 7439 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑅↑𝑟𝑛) = (𝑅↑𝑟𝑁)) |
| 22 | 21 | coeq2d 5873 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑅 ∘ (𝑅↑𝑟𝑛)) = (𝑅 ∘ (𝑅↑𝑟𝑁))) |
| 23 | 20, 22 | eqeq12d 2753 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑅↑𝑟(𝑛 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑛)) ↔ (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))) |
| 24 | 23 | imbi2d 340 |
. . 3
⊢ (𝑛 = 𝑁 → ((𝑅 ∈ 𝑉 → (𝑅↑𝑟(𝑛 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑛))) ↔ (𝑅 ∈ 𝑉 → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁))))) |
| 25 | | relexp1g 15065 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) |
| 26 | 25 | coeq1d 5872 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟1) ∘ 𝑅) = (𝑅 ∘ 𝑅)) |
| 27 | | 1nn 12277 |
. . . . 5
⊢ 1 ∈
ℕ |
| 28 | | relexpsucnnr 15064 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 1 ∈ ℕ) → (𝑅↑𝑟(1 +
1)) = ((𝑅↑𝑟1) ∘ 𝑅)) |
| 29 | 27, 28 | mpan2 691 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟(1 + 1)) = ((𝑅↑𝑟1)
∘ 𝑅)) |
| 30 | 25 | coeq2d 5873 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∘ (𝑅↑𝑟1)) = (𝑅 ∘ 𝑅)) |
| 31 | 26, 29, 30 | 3eqtr4d 2787 |
. . 3
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟(1 + 1)) = (𝑅 ∘ (𝑅↑𝑟1))) |
| 32 | | coeq1 5868 |
. . . . . . . . 9
⊢ ((𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚)) → ((𝑅↑𝑟(𝑚 + 1)) ∘ 𝑅) = ((𝑅 ∘ (𝑅↑𝑟𝑚)) ∘ 𝑅)) |
| 33 | | coass 6285 |
. . . . . . . . 9
⊢ ((𝑅 ∘ (𝑅↑𝑟𝑚)) ∘ 𝑅) = (𝑅 ∘ ((𝑅↑𝑟𝑚) ∘ 𝑅)) |
| 34 | 32, 33 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚)) → ((𝑅↑𝑟(𝑚 + 1)) ∘ 𝑅) = (𝑅 ∘ ((𝑅↑𝑟𝑚) ∘ 𝑅))) |
| 35 | 34 | adantl 481 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) ∧ (𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚))) → ((𝑅↑𝑟(𝑚 + 1)) ∘ 𝑅) = (𝑅 ∘ ((𝑅↑𝑟𝑚) ∘ 𝑅))) |
| 36 | | simpl 482 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) ∧ (𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚))) → (𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ)) |
| 37 | | peano2nn 12278 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
| 38 | 37 | anim2i 617 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) → (𝑅 ∈ 𝑉 ∧ (𝑚 + 1) ∈ ℕ)) |
| 39 | | relexpsucnnr 15064 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑚 + 1) ∈ ℕ) → (𝑅↑𝑟((𝑚 + 1) + 1)) = ((𝑅↑𝑟(𝑚 + 1)) ∘ 𝑅)) |
| 40 | 36, 38, 39 | 3syl 18 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) ∧ (𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚))) → (𝑅↑𝑟((𝑚 + 1) + 1)) = ((𝑅↑𝑟(𝑚 + 1)) ∘ 𝑅)) |
| 41 | | relexpsucnnr 15064 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) → (𝑅↑𝑟(𝑚 + 1)) = ((𝑅↑𝑟𝑚) ∘ 𝑅)) |
| 42 | 41 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) ∧ (𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚))) → (𝑅↑𝑟(𝑚 + 1)) = ((𝑅↑𝑟𝑚) ∘ 𝑅)) |
| 43 | 42 | coeq2d 5873 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) ∧ (𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚))) → (𝑅 ∘ (𝑅↑𝑟(𝑚 + 1))) = (𝑅 ∘ ((𝑅↑𝑟𝑚) ∘ 𝑅))) |
| 44 | 35, 40, 43 | 3eqtr4d 2787 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) ∧ (𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚))) → (𝑅↑𝑟((𝑚 + 1) + 1)) = (𝑅 ∘ (𝑅↑𝑟(𝑚 + 1)))) |
| 45 | 44 | ex 412 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) → ((𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚)) → (𝑅↑𝑟((𝑚 + 1) + 1)) = (𝑅 ∘ (𝑅↑𝑟(𝑚 + 1))))) |
| 46 | 45 | expcom 413 |
. . . 4
⊢ (𝑚 ∈ ℕ → (𝑅 ∈ 𝑉 → ((𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚)) → (𝑅↑𝑟((𝑚 + 1) + 1)) = (𝑅 ∘ (𝑅↑𝑟(𝑚 + 1)))))) |
| 47 | 46 | a2d 29 |
. . 3
⊢ (𝑚 ∈ ℕ → ((𝑅 ∈ 𝑉 → (𝑅↑𝑟(𝑚 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑚))) → (𝑅 ∈ 𝑉 → (𝑅↑𝑟((𝑚 + 1) + 1)) = (𝑅 ∘ (𝑅↑𝑟(𝑚 + 1)))))) |
| 48 | 6, 12, 18, 24, 31, 47 | nnind 12284 |
. 2
⊢ (𝑁 ∈ ℕ → (𝑅 ∈ 𝑉 → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁)))) |
| 49 | 48 | impcom 407 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑅↑𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑁))) |