Step | Hyp | Ref
| Expression |
1 | | itcoval 45959 |
. . . 4
⊢ (𝐹 ∈ 𝑉 → (IterComp‘𝐹) = seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))) |
2 | 1 | fveq1d 6770 |
. . 3
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘1) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘1)) |
3 | 2 | adantl 481 |
. 2
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘1)) |
4 | | nn0uz 12602 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
5 | | 0nn0 12231 |
. . . . 5
⊢ 0 ∈
ℕ0 |
6 | 5 | a1i 11 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → 0 ∈
ℕ0) |
7 | | 1e0p1 12461 |
. . . 4
⊢ 1 = (0 +
1) |
8 | 1 | eqcomd 2745 |
. . . . . . 7
⊢ (𝐹 ∈ 𝑉 → seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))) = (IterComp‘𝐹)) |
9 | 8 | fveq1d 6770 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘0) = ((IterComp‘𝐹)‘0)) |
10 | | itcoval0 45960 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹)) |
11 | 9, 10 | eqtrd 2779 |
. . . . 5
⊢ (𝐹 ∈ 𝑉 → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘0) = ( I ↾ dom 𝐹)) |
12 | 11 | adantl 481 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘0) = ( I ↾ dom 𝐹)) |
13 | | eqidd 2740 |
. . . . 5
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))) |
14 | | ax-1ne0 10924 |
. . . . . . . . 9
⊢ 1 ≠
0 |
15 | 14 | neii 2946 |
. . . . . . . 8
⊢ ¬ 1
= 0 |
16 | | eqeq1 2743 |
. . . . . . . 8
⊢ (𝑖 = 1 → (𝑖 = 0 ↔ 1 = 0)) |
17 | 15, 16 | mtbiri 326 |
. . . . . . 7
⊢ (𝑖 = 1 → ¬ 𝑖 = 0) |
18 | 17 | iffalsed 4475 |
. . . . . 6
⊢ (𝑖 = 1 → if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹) = 𝐹) |
19 | 18 | adantl 481 |
. . . . 5
⊢ (((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ 𝑖 = 1) → if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹) = 𝐹) |
20 | | 1nn0 12232 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
21 | 20 | a1i 11 |
. . . . 5
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → 1 ∈
ℕ0) |
22 | | simpr 484 |
. . . . 5
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → 𝐹 ∈ 𝑉) |
23 | 13, 19, 21, 22 | fvmptd 6876 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))‘1) = 𝐹) |
24 | 4, 6, 7, 12, 23 | seqp1d 13719 |
. . 3
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘1) = (( I ↾ dom 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹)) |
25 | | eqidd 2740 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → (𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)) = (𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))) |
26 | | coeq2 5764 |
. . . . . . 7
⊢ (𝑔 = ( I ↾ dom 𝐹) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ( I ↾ dom 𝐹))) |
27 | 26 | ad2antrl 724 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑉 ∧ (𝑔 = ( I ↾ dom 𝐹) ∧ 𝑗 = 𝐹)) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ( I ↾ dom 𝐹))) |
28 | | dmexg 7737 |
. . . . . . 7
⊢ (𝐹 ∈ 𝑉 → dom 𝐹 ∈ V) |
29 | 28 | resiexd 7086 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → ( I ↾ dom 𝐹) ∈ V) |
30 | | elex 3448 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → 𝐹 ∈ V) |
31 | | coexg 7763 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑉 ∧ ( I ↾ dom 𝐹) ∈ V) → (𝐹 ∘ ( I ↾ dom 𝐹)) ∈ V) |
32 | 29, 31 | mpdan 683 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∘ ( I ↾ dom 𝐹)) ∈ V) |
33 | 25, 27, 29, 30, 32 | ovmpod 7416 |
. . . . 5
⊢ (𝐹 ∈ 𝑉 → (( I ↾ dom 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹) = (𝐹 ∘ ( I ↾ dom 𝐹))) |
34 | 33 | adantl 481 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (( I ↾ dom 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹) = (𝐹 ∘ ( I ↾ dom 𝐹))) |
35 | | coires1 6165 |
. . . . 5
⊢ (𝐹 ∘ ( I ↾ dom 𝐹)) = (𝐹 ↾ dom 𝐹) |
36 | | resdm 5933 |
. . . . . 6
⊢ (Rel
𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) |
37 | 36 | adantr 480 |
. . . . 5
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (𝐹 ↾ dom 𝐹) = 𝐹) |
38 | 35, 37 | eqtrid 2791 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (𝐹 ∘ ( I ↾ dom 𝐹)) = 𝐹) |
39 | 34, 38 | eqtrd 2779 |
. . 3
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (( I ↾ dom 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹) = 𝐹) |
40 | 24, 39 | eqtrd 2779 |
. 2
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘1) = 𝐹) |
41 | 3, 40 | eqtrd 2779 |
1
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = 𝐹) |