Step |
Hyp |
Ref |
Expression |
1 |
|
itcoval |
⊢ ( 𝐹 ∈ 𝑉 → ( IterComp ‘ 𝐹 ) = seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ) |
2 |
1
|
fveq1d |
⊢ ( 𝐹 ∈ 𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ 1 ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 1 ) ) |
3 |
2
|
adantl |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( IterComp ‘ 𝐹 ) ‘ 1 ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 1 ) ) |
4 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
5 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
6 |
5
|
a1i |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → 0 ∈ ℕ0 ) |
7 |
|
1e0p1 |
⊢ 1 = ( 0 + 1 ) |
8 |
1
|
eqcomd |
⊢ ( 𝐹 ∈ 𝑉 → seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) = ( IterComp ‘ 𝐹 ) ) |
9 |
8
|
fveq1d |
⊢ ( 𝐹 ∈ 𝑉 → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 0 ) = ( ( IterComp ‘ 𝐹 ) ‘ 0 ) ) |
10 |
|
itcoval0 |
⊢ ( 𝐹 ∈ 𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( I ↾ dom 𝐹 ) ) |
11 |
9 10
|
eqtrd |
⊢ ( 𝐹 ∈ 𝑉 → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 0 ) = ( I ↾ dom 𝐹 ) ) |
12 |
11
|
adantl |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 0 ) = ( I ↾ dom 𝐹 ) ) |
13 |
|
eqidd |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) |
14 |
|
ax-1ne0 |
⊢ 1 ≠ 0 |
15 |
14
|
neii |
⊢ ¬ 1 = 0 |
16 |
|
eqeq1 |
⊢ ( 𝑖 = 1 → ( 𝑖 = 0 ↔ 1 = 0 ) ) |
17 |
15 16
|
mtbiri |
⊢ ( 𝑖 = 1 → ¬ 𝑖 = 0 ) |
18 |
17
|
iffalsed |
⊢ ( 𝑖 = 1 → if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) = 𝐹 ) |
19 |
18
|
adantl |
⊢ ( ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑖 = 1 ) → if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) = 𝐹 ) |
20 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
21 |
20
|
a1i |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → 1 ∈ ℕ0 ) |
22 |
|
simpr |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → 𝐹 ∈ 𝑉 ) |
23 |
13 19 21 22
|
fvmptd |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ‘ 1 ) = 𝐹 ) |
24 |
4 6 7 12 23
|
seqp1d |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 1 ) = ( ( I ↾ dom 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) ) |
25 |
|
eqidd |
⊢ ( 𝐹 ∈ 𝑉 → ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) = ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) ) |
26 |
|
coeq2 |
⊢ ( 𝑔 = ( I ↾ dom 𝐹 ) → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) ) |
27 |
26
|
ad2antrl |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ ( 𝑔 = ( I ↾ dom 𝐹 ) ∧ 𝑗 = 𝐹 ) ) → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) ) |
28 |
|
dmexg |
⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V ) |
29 |
28
|
resiexd |
⊢ ( 𝐹 ∈ 𝑉 → ( I ↾ dom 𝐹 ) ∈ V ) |
30 |
|
elex |
⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V ) |
31 |
|
coexg |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ ( I ↾ dom 𝐹 ) ∈ V ) → ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) ∈ V ) |
32 |
29 31
|
mpdan |
⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) ∈ V ) |
33 |
25 27 29 30 32
|
ovmpod |
⊢ ( 𝐹 ∈ 𝑉 → ( ( I ↾ dom 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) = ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) ) |
34 |
33
|
adantl |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( I ↾ dom 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) = ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) ) |
35 |
|
coires1 |
⊢ ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) = ( 𝐹 ↾ dom 𝐹 ) |
36 |
|
resdm |
⊢ ( Rel 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 ) |
37 |
36
|
adantr |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 ) |
38 |
35 37
|
syl5eq |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) = 𝐹 ) |
39 |
34 38
|
eqtrd |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( I ↾ dom 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) = 𝐹 ) |
40 |
24 39
|
eqtrd |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 1 ) = 𝐹 ) |
41 |
3 40
|
eqtrd |
⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( IterComp ‘ 𝐹 ) ‘ 1 ) = 𝐹 ) |