| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elnn0 12528 | . . 3
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) | 
| 2 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑛 = 1 → (𝑅↑𝑟𝑛) = (𝑅↑𝑟1)) | 
| 3 | 2 | cnveqd 5886 | . . . . . . 7
⊢ (𝑛 = 1 → ◡(𝑅↑𝑟𝑛) = ◡(𝑅↑𝑟1)) | 
| 4 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑛 = 1 → (◡𝑅↑𝑟𝑛) = (◡𝑅↑𝑟1)) | 
| 5 | 3, 4 | eqeq12d 2753 | . . . . . 6
⊢ (𝑛 = 1 → (◡(𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑛) ↔ ◡(𝑅↑𝑟1) = (◡𝑅↑𝑟1))) | 
| 6 | 5 | imbi2d 340 | . . . . 5
⊢ (𝑛 = 1 → ((𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑛)) ↔ (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟1) = (◡𝑅↑𝑟1)))) | 
| 7 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑅↑𝑟𝑛) = (𝑅↑𝑟𝑚)) | 
| 8 | 7 | cnveqd 5886 | . . . . . . 7
⊢ (𝑛 = 𝑚 → ◡(𝑅↑𝑟𝑛) = ◡(𝑅↑𝑟𝑚)) | 
| 9 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑛 = 𝑚 → (◡𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑚)) | 
| 10 | 8, 9 | eqeq12d 2753 | . . . . . 6
⊢ (𝑛 = 𝑚 → (◡(𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑛) ↔ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚))) | 
| 11 | 10 | imbi2d 340 | . . . . 5
⊢ (𝑛 = 𝑚 → ((𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑛)) ↔ (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)))) | 
| 12 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑛 = (𝑚 + 1) → (𝑅↑𝑟𝑛) = (𝑅↑𝑟(𝑚 + 1))) | 
| 13 | 12 | cnveqd 5886 | . . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → ◡(𝑅↑𝑟𝑛) = ◡(𝑅↑𝑟(𝑚 + 1))) | 
| 14 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → (◡𝑅↑𝑟𝑛) = (◡𝑅↑𝑟(𝑚 + 1))) | 
| 15 | 13, 14 | eqeq12d 2753 | . . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (◡(𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑛) ↔ ◡(𝑅↑𝑟(𝑚 + 1)) = (◡𝑅↑𝑟(𝑚 + 1)))) | 
| 16 | 15 | imbi2d 340 | . . . . 5
⊢ (𝑛 = (𝑚 + 1) → ((𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑛)) ↔ (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟(𝑚 + 1)) = (◡𝑅↑𝑟(𝑚 + 1))))) | 
| 17 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑅↑𝑟𝑛) = (𝑅↑𝑟𝑁)) | 
| 18 | 17 | cnveqd 5886 | . . . . . . 7
⊢ (𝑛 = 𝑁 → ◡(𝑅↑𝑟𝑛) = ◡(𝑅↑𝑟𝑁)) | 
| 19 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑛 = 𝑁 → (◡𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑁)) | 
| 20 | 18, 19 | eqeq12d 2753 | . . . . . 6
⊢ (𝑛 = 𝑁 → (◡(𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑛) ↔ ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))) | 
| 21 | 20 | imbi2d 340 | . . . . 5
⊢ (𝑛 = 𝑁 → ((𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑛) = (◡𝑅↑𝑟𝑛)) ↔ (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)))) | 
| 22 |  | relexp1g 15065 | . . . . . . 7
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) | 
| 23 | 22 | cnveqd 5886 | . . . . . 6
⊢ (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟1) = ◡𝑅) | 
| 24 |  | cnvexg 7946 | . . . . . . 7
⊢ (𝑅 ∈ 𝑉 → ◡𝑅 ∈ V) | 
| 25 |  | relexp1g 15065 | . . . . . . 7
⊢ (◡𝑅 ∈ V → (◡𝑅↑𝑟1) = ◡𝑅) | 
| 26 | 24, 25 | syl 17 | . . . . . 6
⊢ (𝑅 ∈ 𝑉 → (◡𝑅↑𝑟1) = ◡𝑅) | 
| 27 | 23, 26 | eqtr4d 2780 | . . . . 5
⊢ (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟1) = (◡𝑅↑𝑟1)) | 
| 28 |  | cnvco 5896 | . . . . . . . . 9
⊢ ◡((𝑅↑𝑟𝑚) ∘ 𝑅) = (◡𝑅 ∘ ◡(𝑅↑𝑟𝑚)) | 
| 29 |  | simp3 1139 | . . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) | 
| 30 | 29 | coeq2d 5873 | . . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → (◡𝑅 ∘ ◡(𝑅↑𝑟𝑚)) = (◡𝑅 ∘ (◡𝑅↑𝑟𝑚))) | 
| 31 | 28, 30 | eqtrid 2789 | . . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → ◡((𝑅↑𝑟𝑚) ∘ 𝑅) = (◡𝑅 ∘ (◡𝑅↑𝑟𝑚))) | 
| 32 |  | simp2 1138 | . . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → 𝑅 ∈ 𝑉) | 
| 33 |  | simp1 1137 | . . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → 𝑚 ∈ ℕ) | 
| 34 |  | relexpsucnnr 15064 | . . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) → (𝑅↑𝑟(𝑚 + 1)) = ((𝑅↑𝑟𝑚) ∘ 𝑅)) | 
| 35 | 32, 33, 34 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → (𝑅↑𝑟(𝑚 + 1)) = ((𝑅↑𝑟𝑚) ∘ 𝑅)) | 
| 36 | 35 | cnveqd 5886 | . . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → ◡(𝑅↑𝑟(𝑚 + 1)) = ◡((𝑅↑𝑟𝑚) ∘ 𝑅)) | 
| 37 | 32, 24 | syl 17 | . . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → ◡𝑅 ∈ V) | 
| 38 |  | relexpsucnnl 15069 | . . . . . . . . 9
⊢ ((◡𝑅 ∈ V ∧ 𝑚 ∈ ℕ) → (◡𝑅↑𝑟(𝑚 + 1)) = (◡𝑅 ∘ (◡𝑅↑𝑟𝑚))) | 
| 39 | 37, 33, 38 | syl2anc 584 | . . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → (◡𝑅↑𝑟(𝑚 + 1)) = (◡𝑅 ∘ (◡𝑅↑𝑟𝑚))) | 
| 40 | 31, 36, 39 | 3eqtr4d 2787 | . . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → ◡(𝑅↑𝑟(𝑚 + 1)) = (◡𝑅↑𝑟(𝑚 + 1))) | 
| 41 | 40 | 3exp 1120 | . . . . . 6
⊢ (𝑚 ∈ ℕ → (𝑅 ∈ 𝑉 → (◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚) → ◡(𝑅↑𝑟(𝑚 + 1)) = (◡𝑅↑𝑟(𝑚 + 1))))) | 
| 42 | 41 | a2d 29 | . . . . 5
⊢ (𝑚 ∈ ℕ → ((𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑚) = (◡𝑅↑𝑟𝑚)) → (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟(𝑚 + 1)) = (◡𝑅↑𝑟(𝑚 + 1))))) | 
| 43 | 6, 11, 16, 21, 27, 42 | nnind 12284 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))) | 
| 44 |  | cnvresid 6645 | . . . . . . 7
⊢ ◡( I ↾ (dom 𝑅 ∪ ran 𝑅)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)) | 
| 45 |  | uncom 4158 | . . . . . . . . 9
⊢ (dom
𝑅 ∪ ran 𝑅) = (ran 𝑅 ∪ dom 𝑅) | 
| 46 |  | df-rn 5696 | . . . . . . . . . 10
⊢ ran 𝑅 = dom ◡𝑅 | 
| 47 |  | dfdm4 5906 | . . . . . . . . . 10
⊢ dom 𝑅 = ran ◡𝑅 | 
| 48 | 46, 47 | uneq12i 4166 | . . . . . . . . 9
⊢ (ran
𝑅 ∪ dom 𝑅) = (dom ◡𝑅 ∪ ran ◡𝑅) | 
| 49 | 45, 48 | eqtri 2765 | . . . . . . . 8
⊢ (dom
𝑅 ∪ ran 𝑅) = (dom ◡𝑅 ∪ ran ◡𝑅) | 
| 50 | 49 | reseq2i 5994 | . . . . . . 7
⊢ ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = ( I ↾ (dom
◡𝑅 ∪ ran ◡𝑅)) | 
| 51 | 44, 50 | eqtri 2765 | . . . . . 6
⊢ ◡( I ↾ (dom 𝑅 ∪ ran 𝑅)) = ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅)) | 
| 52 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑁 = 0 → (𝑅↑𝑟𝑁) = (𝑅↑𝑟0)) | 
| 53 |  | relexp0g 15061 | . . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) | 
| 54 | 52, 53 | sylan9eq 2797 | . . . . . . 7
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑁) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) | 
| 55 | 54 | cnveqd 5886 | . . . . . 6
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = ◡( I ↾ (dom 𝑅 ∪ ran 𝑅))) | 
| 56 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑁 = 0 → (◡𝑅↑𝑟𝑁) = (◡𝑅↑𝑟0)) | 
| 57 | 56 | adantr 480 | . . . . . . 7
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (◡𝑅↑𝑟𝑁) = (◡𝑅↑𝑟0)) | 
| 58 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ 𝑉) | 
| 59 |  | relexp0g 15061 | . . . . . . . 8
⊢ (◡𝑅 ∈ V → (◡𝑅↑𝑟0) = ( I ↾
(dom ◡𝑅 ∪ ran ◡𝑅))) | 
| 60 | 58, 24, 59 | 3syl 18 | . . . . . . 7
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (◡𝑅↑𝑟0) = ( I ↾
(dom ◡𝑅 ∪ ran ◡𝑅))) | 
| 61 | 57, 60 | eqtrd 2777 | . . . . . 6
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → (◡𝑅↑𝑟𝑁) = ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅))) | 
| 62 | 51, 55, 61 | 3eqtr4a 2803 | . . . . 5
⊢ ((𝑁 = 0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)) | 
| 63 | 62 | ex 412 | . . . 4
⊢ (𝑁 = 0 → (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))) | 
| 64 | 43, 63 | jaoi 858 | . . 3
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))) | 
| 65 | 1, 64 | sylbi 217 | . 2
⊢ (𝑁 ∈ ℕ0
→ (𝑅 ∈ 𝑉 → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁))) | 
| 66 | 65 | imp 406 | 1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)) |