Step | Hyp | Ref
| Expression |
1 | | itcoval 45680 |
. . . 4
⊢ (𝐹 ∈ 𝑉 → (IterComp‘𝐹) = seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))) |
2 | 1 | fveq1d 6719 |
. . 3
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘3) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘3)) |
3 | 2 | adantl 485 |
. 2
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘3) = (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘3)) |
4 | | nn0uz 12476 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
5 | | 2nn0 12107 |
. . . 4
⊢ 2 ∈
ℕ0 |
6 | 5 | a1i 11 |
. . 3
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → 2 ∈
ℕ0) |
7 | | df-3 11894 |
. . 3
⊢ 3 = (2 +
1) |
8 | 1 | eqcomd 2743 |
. . . . . 6
⊢ (𝐹 ∈ 𝑉 → seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))) = (IterComp‘𝐹)) |
9 | 8 | fveq1d 6719 |
. . . . 5
⊢ (𝐹 ∈ 𝑉 → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘2) = ((IterComp‘𝐹)‘2)) |
10 | 9 | adantl 485 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘2) = ((IterComp‘𝐹)‘2)) |
11 | | itcoval2 45683 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘2) = (𝐹 ∘ 𝐹)) |
12 | 10, 11 | eqtrd 2777 |
. . 3
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘2) = (𝐹 ∘ 𝐹)) |
13 | | eqidd 2738 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))) |
14 | | 3ne0 11936 |
. . . . . . . 8
⊢ 3 ≠
0 |
15 | | neeq1 3003 |
. . . . . . . 8
⊢ (𝑖 = 3 → (𝑖 ≠ 0 ↔ 3 ≠ 0)) |
16 | 14, 15 | mpbiri 261 |
. . . . . . 7
⊢ (𝑖 = 3 → 𝑖 ≠ 0) |
17 | 16 | neneqd 2945 |
. . . . . 6
⊢ (𝑖 = 3 → ¬ 𝑖 = 0) |
18 | 17 | iffalsed 4450 |
. . . . 5
⊢ (𝑖 = 3 → if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹) = 𝐹) |
19 | 18 | adantl 485 |
. . . 4
⊢ (((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) ∧ 𝑖 = 3) → if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹) = 𝐹) |
20 | | 3nn0 12108 |
. . . . 5
⊢ 3 ∈
ℕ0 |
21 | 20 | a1i 11 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → 3 ∈
ℕ0) |
22 | | simpr 488 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → 𝐹 ∈ 𝑉) |
23 | 13, 19, 21, 22 | fvmptd 6825 |
. . 3
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))‘3) = 𝐹) |
24 | 4, 6, 7, 12, 23 | seqp1d 13591 |
. 2
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → (seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))‘3) = ((𝐹 ∘ 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹)) |
25 | | eqidd 2738 |
. . . 4
⊢ (𝐹 ∈ 𝑉 → (𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)) = (𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))) |
26 | | coeq2 5727 |
. . . . 5
⊢ (𝑔 = (𝐹 ∘ 𝐹) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝐹 ∘ 𝐹))) |
27 | 26 | ad2antrl 728 |
. . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ (𝑔 = (𝐹 ∘ 𝐹) ∧ 𝑗 = 𝐹)) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝐹 ∘ 𝐹))) |
28 | | coexg 7707 |
. . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉) → (𝐹 ∘ 𝐹) ∈ V) |
29 | 28 | anidms 570 |
. . . 4
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∘ 𝐹) ∈ V) |
30 | | elex 3426 |
. . . 4
⊢ (𝐹 ∈ 𝑉 → 𝐹 ∈ V) |
31 | | coexg 7707 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑉 ∧ (𝐹 ∘ 𝐹) ∈ V) → (𝐹 ∘ (𝐹 ∘ 𝐹)) ∈ V) |
32 | 28, 31 | syldan 594 |
. . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉) → (𝐹 ∘ (𝐹 ∘ 𝐹)) ∈ V) |
33 | 32 | anidms 570 |
. . . 4
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∘ (𝐹 ∘ 𝐹)) ∈ V) |
34 | 25, 27, 29, 30, 33 | ovmpod 7361 |
. . 3
⊢ (𝐹 ∈ 𝑉 → ((𝐹 ∘ 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹) = (𝐹 ∘ (𝐹 ∘ 𝐹))) |
35 | 34 | adantl 485 |
. 2
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((𝐹 ∘ 𝐹)(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹) = (𝐹 ∘ (𝐹 ∘ 𝐹))) |
36 | 3, 24, 35 | 3eqtrd 2781 |
1
⊢ ((Rel
𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) |