Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = 0 → (( I ↾ 𝐴)↑𝑟𝑥) = (( I ↾ 𝐴)↑𝑟0)) |
2 | 1 | eqeq1d 2612 |
. . . 4
⊢ (𝑥 = 0 → ((( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴) ↔ (( I ↾ 𝐴)↑𝑟0) =
( I ↾ 𝐴))) |
3 | 2 | imbi2d 329 |
. . 3
⊢ (𝑥 = 0 → ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴)) ↔ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟0) = ( I ↾
𝐴)))) |
4 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = 𝑦 → (( I ↾ 𝐴)↑𝑟𝑥) = (( I ↾ 𝐴)↑𝑟𝑦)) |
5 | 4 | eqeq1d 2612 |
. . . 4
⊢ (𝑥 = 𝑦 → ((( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴) ↔ (( I ↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴))) |
6 | 5 | imbi2d 329 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴)) ↔ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴)))) |
7 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (( I ↾ 𝐴)↑𝑟𝑥) = (( I ↾ 𝐴)↑𝑟(𝑦 + 1))) |
8 | 7 | eqeq1d 2612 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴) ↔ (( I ↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴))) |
9 | 8 | imbi2d 329 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴)) ↔ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)))) |
10 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = 𝑁 → (( I ↾ 𝐴)↑𝑟𝑥) = (( I ↾ 𝐴)↑𝑟𝑁)) |
11 | 10 | eqeq1d 2612 |
. . . 4
⊢ (𝑥 = 𝑁 → ((( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴) ↔ (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴))) |
12 | 11 | imbi2d 329 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴)) ↔ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴)))) |
13 | | resiexg 6994 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
14 | | relexp0g 13610 |
. . . . 5
⊢ (( I
↾ 𝐴) ∈ V →
(( I ↾ 𝐴)↑𝑟0) = ( I ↾
(dom ( I ↾ 𝐴) ∪
ran ( I ↾ 𝐴)))) |
15 | 13, 14 | syl 17 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟0) = ( I ↾
(dom ( I ↾ 𝐴) ∪
ran ( I ↾ 𝐴)))) |
16 | | dmresi 5376 |
. . . . . . 7
⊢ dom ( I
↾ 𝐴) = 𝐴 |
17 | | rnresi 5398 |
. . . . . . 7
⊢ ran ( I
↾ 𝐴) = 𝐴 |
18 | 16, 17 | uneq12i 3727 |
. . . . . 6
⊢ (dom ( I
↾ 𝐴) ∪ ran ( I
↾ 𝐴)) = (𝐴 ∪ 𝐴) |
19 | | unidm 3718 |
. . . . . 6
⊢ (𝐴 ∪ 𝐴) = 𝐴 |
20 | 18, 19 | eqtri 2632 |
. . . . 5
⊢ (dom ( I
↾ 𝐴) ∪ ran ( I
↾ 𝐴)) = 𝐴 |
21 | 20 | reseq2i 5314 |
. . . 4
⊢ ( I
↾ (dom ( I ↾ 𝐴)
∪ ran ( I ↾ 𝐴)))
= ( I ↾ 𝐴) |
22 | 15, 21 | syl6eq 2660 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟0) = ( I ↾
𝐴)) |
23 | | relres 5346 |
. . . . . . . . . 10
⊢ Rel ( I
↾ 𝐴) |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉) → Rel ( I ↾ 𝐴)) |
25 | 13 | adantl 481 |
. . . . . . . . 9
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉) → ( I ↾ 𝐴) ∈ V) |
26 | 24, 25 | relexpsucrd 13618 |
. . . . . . . 8
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉) → (𝑦 ∈ ℕ0 → (( I
↾ 𝐴)↑𝑟(𝑦 + 1)) = ((( I ↾ 𝐴)↑𝑟𝑦) ∘ ( I ↾ 𝐴)))) |
27 | 26 | 3impia 1253 |
. . . . . . 7
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → (( I
↾ 𝐴)↑𝑟(𝑦 + 1)) = ((( I ↾ 𝐴)↑𝑟𝑦) ∘ ( I ↾ 𝐴))) |
28 | | simp1 1054 |
. . . . . . . . 9
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → (( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴)) |
29 | 28 | coeq1d 5205 |
. . . . . . . 8
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → ((( I
↾ 𝐴)↑𝑟𝑦) ∘ ( I ↾ 𝐴)) = (( I ↾ 𝐴) ∘ ( I ↾ 𝐴))) |
30 | | coires1 5570 |
. . . . . . . . 9
⊢ (( I
↾ 𝐴) ∘ ( I
↾ 𝐴)) = (( I ↾
𝐴) ↾ 𝐴) |
31 | | residm 5350 |
. . . . . . . . 9
⊢ (( I
↾ 𝐴) ↾ 𝐴) = ( I ↾ 𝐴) |
32 | 30, 31 | eqtri 2632 |
. . . . . . . 8
⊢ (( I
↾ 𝐴) ∘ ( I
↾ 𝐴)) = ( I ↾
𝐴) |
33 | 29, 32 | syl6eq 2660 |
. . . . . . 7
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → ((( I
↾ 𝐴)↑𝑟𝑦) ∘ ( I ↾ 𝐴)) = ( I ↾ 𝐴)) |
34 | 27, 33 | eqtrd 2644 |
. . . . . 6
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → (( I
↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)) |
35 | 34 | 3exp 1256 |
. . . . 5
⊢ ((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) → (𝐴 ∈ 𝑉 → (𝑦 ∈ ℕ0 → (( I
↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)))) |
36 | 35 | com13 86 |
. . . 4
⊢ (𝑦 ∈ ℕ0
→ (𝐴 ∈ 𝑉 → ((( I ↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) → (( I ↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)))) |
37 | 36 | a2d 29 |
. . 3
⊢ (𝑦 ∈ ℕ0
→ ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴)) → (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)))) |
38 | 3, 6, 9, 12, 22, 37 | nn0ind 11348 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴))) |
39 | 38 | impcom 445 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (( I
↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴)) |