Step | Hyp | Ref
| Expression |
1 | | itcoval 45425 |
. . . 4
⊢ (𝐹 ∈ 𝑉 → (IterComp‘𝐹) = seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))) |
2 | 1 | fveq1d 6653 |
. . 3
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘1) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘1)) |
3 | 2 | adantl 486 |
. 2
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘1)) |
4 | | nn0uz 12305 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
5 | | 0nn0 11934 |
. . . . 5
⊢ 0 ∈
ℕ0 |
6 | 5 | a1i 11 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → 0 ∈
ℕ0) |
7 | | 1e0p1 12164 |
. . . 4
⊢ 1 = (0 +
1) |
8 | 1 | eqcomd 2765 |
. . . . . . 7
⊢ (𝐹 ∈ 𝑉 → seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))) = (IterComp‘𝐹)) |
9 | 8 | fveq1d 6653 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘0) = ((IterComp‘𝐹)‘0)) |
10 | | itcoval0 45426 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹)) |
11 | 9, 10 | eqtrd 2794 |
. . . . 5
⊢ (𝐹 ∈ 𝑉 → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘0) = ( I ↾ dom 𝐹)) |
12 | 11 | adantl 486 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘0) = ( I ↾ dom 𝐹)) |
13 | | eqidd 2760 |
. . . . 5
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))) |
14 | | ax-1ne0 10629 |
. . . . . . . . 9
⊢ 1 ≠
0 |
15 | 14 | neii 2951 |
. . . . . . . 8
⊢ ¬ 1
= 0 |
16 | | eqeq1 2763 |
. . . . . . . 8
⊢ (𝑖 = 1 → (𝑖 = 0 ↔ 1 = 0)) |
17 | 15, 16 | mtbiri 331 |
. . . . . . 7
⊢ (𝑖 = 1 → ¬ 𝑖 = 0) |
18 | 17 | iffalsed 4424 |
. . . . . 6
⊢ (𝑖 = 1 → if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹) = 𝐹) |
19 | 18 | adantl 486 |
. . . . 5
⊢ (((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ 𝑖 = 1) → if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹) = 𝐹) |
20 | | 1nn0 11935 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
21 | 20 | a1i 11 |
. . . . 5
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → 1 ∈
ℕ0) |
22 | | simpr 489 |
. . . . 5
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → 𝐹 ∈ 𝑉) |
23 | 13, 19, 21, 22 | fvmptd 6759 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))‘1) = 𝐹) |
24 | 4, 6, 7, 12, 23 | seqp1d 13420 |
. . 3
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘1) = (( I ↾ dom 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹)) |
25 | | eqidd 2760 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → (𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)) = (𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))) |
26 | | coeq2 5691 |
. . . . . . 7
⊢ (𝑔 = ( I ↾ dom 𝐹) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ( I ↾ dom 𝐹))) |
27 | 26 | ad2antrl 728 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑉 ∧ (𝑔 = ( I ↾ dom 𝐹) ∧ 𝑗 = 𝐹)) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ( I ↾ dom 𝐹))) |
28 | | dmexg 7606 |
. . . . . . 7
⊢ (𝐹 ∈ 𝑉 → dom 𝐹 ∈ V) |
29 | 28 | resiexd 6963 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → ( I ↾ dom 𝐹) ∈ V) |
30 | | elex 3427 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → 𝐹 ∈ V) |
31 | | coexg 7632 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑉 ∧ ( I ↾ dom 𝐹) ∈ V) → (𝐹 ∘ ( I ↾ dom 𝐹)) ∈ V) |
32 | 29, 31 | mpdan 687 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∘ ( I ↾ dom 𝐹)) ∈ V) |
33 | 25, 27, 29, 30, 32 | ovmpod 7290 |
. . . . 5
⊢ (𝐹 ∈ 𝑉 → (( I ↾ dom 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹) = (𝐹 ∘ ( I ↾ dom 𝐹))) |
34 | 33 | adantl 486 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (( I ↾ dom 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹) = (𝐹 ∘ ( I ↾ dom 𝐹))) |
35 | | coires1 6087 |
. . . . 5
⊢ (𝐹 ∘ ( I ↾ dom 𝐹)) = (𝐹 ↾ dom 𝐹) |
36 | | resdm 5861 |
. . . . . 6
⊢ (Rel
𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) |
37 | 36 | adantr 485 |
. . . . 5
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (𝐹 ↾ dom 𝐹) = 𝐹) |
38 | 35, 37 | syl5eq 2806 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (𝐹 ∘ ( I ↾ dom 𝐹)) = 𝐹) |
39 | 34, 38 | eqtrd 2794 |
. . 3
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (( I ↾ dom 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹) = 𝐹) |
40 | 24, 39 | eqtrd 2794 |
. 2
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘1) = 𝐹) |
41 | 3, 40 | eqtrd 2794 |
1
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = 𝐹) |