Step | Hyp | Ref
| Expression |
1 | | oveq2 7277 |
. . . . 5
⊢ (𝑥 = 0 → (( I ↾ 𝐴)↑𝑟𝑥) = (( I ↾ 𝐴)↑𝑟0)) |
2 | 1 | eqeq1d 2742 |
. . . 4
⊢ (𝑥 = 0 → ((( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴) ↔ (( I ↾ 𝐴)↑𝑟0) =
( I ↾ 𝐴))) |
3 | 2 | imbi2d 341 |
. . 3
⊢ (𝑥 = 0 → ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴)) ↔ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟0) = ( I ↾
𝐴)))) |
4 | | oveq2 7277 |
. . . . 5
⊢ (𝑥 = 𝑦 → (( I ↾ 𝐴)↑𝑟𝑥) = (( I ↾ 𝐴)↑𝑟𝑦)) |
5 | 4 | eqeq1d 2742 |
. . . 4
⊢ (𝑥 = 𝑦 → ((( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴) ↔ (( I ↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴))) |
6 | 5 | imbi2d 341 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴)) ↔ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴)))) |
7 | | oveq2 7277 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (( I ↾ 𝐴)↑𝑟𝑥) = (( I ↾ 𝐴)↑𝑟(𝑦 + 1))) |
8 | 7 | eqeq1d 2742 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴) ↔ (( I ↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴))) |
9 | 8 | imbi2d 341 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴)) ↔ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)))) |
10 | | oveq2 7277 |
. . . . 5
⊢ (𝑥 = 𝑁 → (( I ↾ 𝐴)↑𝑟𝑥) = (( I ↾ 𝐴)↑𝑟𝑁)) |
11 | 10 | eqeq1d 2742 |
. . . 4
⊢ (𝑥 = 𝑁 → ((( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴) ↔ (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴))) |
12 | 11 | imbi2d 341 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑥) = ( I ↾ 𝐴)) ↔ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴)))) |
13 | | resiexg 7753 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
14 | | relexp0g 14729 |
. . . . 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 5959 |
. . . . . . 7
⊢ dom ( I
↾ 𝐴) = 𝐴 |
17 | | rnresi 5981 |
. . . . . . 7
⊢ ran ( I
↾ 𝐴) = 𝐴 |
18 | 16, 17 | uneq12i 4100 |
. . . . . 6
⊢ (dom ( I
↾ 𝐴) ∪ ran ( I
↾ 𝐴)) = (𝐴 ∪ 𝐴) |
19 | | unidm 4091 |
. . . . . 6
⊢ (𝐴 ∪ 𝐴) = 𝐴 |
20 | 18, 19 | eqtri 2768 |
. . . . 5
⊢ (dom ( I
↾ 𝐴) ∪ ran ( I
↾ 𝐴)) = 𝐴 |
21 | 20 | reseq2i 5886 |
. . . 4
⊢ ( I
↾ (dom ( I ↾ 𝐴)
∪ ran ( I ↾ 𝐴)))
= ( I ↾ 𝐴) |
22 | 15, 21 | eqtrdi 2796 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟0) = ( I ↾
𝐴)) |
23 | | relres 5918 |
. . . . . . . . 9
⊢ Rel ( I
↾ 𝐴) |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → Rel ( I
↾ 𝐴)) |
25 | | simp3 1137 |
. . . . . . . 8
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈
ℕ0) |
26 | 24, 25 | relexpsucrd 14740 |
. . . . . . 7
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → (( I
↾ 𝐴)↑𝑟(𝑦 + 1)) = ((( I ↾ 𝐴)↑𝑟𝑦) ∘ ( I ↾ 𝐴))) |
27 | | simp1 1135 |
. . . . . . . . 9
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → (( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴)) |
28 | 27 | coeq1d 5768 |
. . . . . . . 8
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → ((( I
↾ 𝐴)↑𝑟𝑦) ∘ ( I ↾ 𝐴)) = (( I ↾ 𝐴) ∘ ( I ↾ 𝐴))) |
29 | | coires1 6166 |
. . . . . . . . 9
⊢ (( I
↾ 𝐴) ∘ ( I
↾ 𝐴)) = (( I ↾
𝐴) ↾ 𝐴) |
30 | | residm 5922 |
. . . . . . . . 9
⊢ (( I
↾ 𝐴) ↾ 𝐴) = ( I ↾ 𝐴) |
31 | 29, 30 | eqtri 2768 |
. . . . . . . 8
⊢ (( I
↾ 𝐴) ∘ ( I
↾ 𝐴)) = ( I ↾
𝐴) |
32 | 28, 31 | eqtrdi 2796 |
. . . . . . 7
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → ((( I
↾ 𝐴)↑𝑟𝑦) ∘ ( I ↾ 𝐴)) = ( I ↾ 𝐴)) |
33 | 26, 32 | eqtrd 2780 |
. . . . . 6
⊢ (((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) ∧ 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) → (( I
↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)) |
34 | 33 | 3exp 1118 |
. . . . 5
⊢ ((( I
↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) → (𝐴 ∈ 𝑉 → (𝑦 ∈ ℕ0 → (( I
↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)))) |
35 | 34 | com13 88 |
. . . 4
⊢ (𝑦 ∈ ℕ0
→ (𝐴 ∈ 𝑉 → ((( I ↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴) → (( I ↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)))) |
36 | 35 | a2d 29 |
. . 3
⊢ (𝑦 ∈ ℕ0
→ ((𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑦) = ( I ↾ 𝐴)) → (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟(𝑦 + 1)) = ( I ↾ 𝐴)))) |
37 | 3, 6, 9, 12, 22, 36 | nn0ind 12413 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴))) |
38 | 37 | impcom 408 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (( I
↾ 𝐴)↑𝑟𝑁) = ( I ↾ 𝐴)) |