This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itcoval

Description: The value of the function that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by AV, 2-May-2024)

Ref Expression
Assertion itcoval ( 𝐹 ∈ 𝑉 → ( IterComp ‘ 𝐹 ) = seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-itco ⊢ IterComp = ( 𝑓 ∈ V ↦ seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝑓 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 ) ) ) )
2 eqidd ⊢ ( 𝑓 = 𝐹 → 0 = 0 )
3 coeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∘ 𝑔 ) = ( 𝐹 ∘ 𝑔 ) )
4 3 mpoeq3dv ⊢ ( 𝑓 = 𝐹 → ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) )
5 dmeq ⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
6 5 reseq2d ⊢ ( 𝑓 = 𝐹 → ( I ↾ dom 𝑓 ) = ( I ↾ dom 𝐹 ) )
7 id ⊢ ( 𝑓 = 𝐹 → 𝑓 = 𝐹 )
8 6 7 ifeq12d ⊢ ( 𝑓 = 𝐹 → if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 ) = if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) )
9 8 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) )
10 2 4 9 seqeq123d ⊢ ( 𝑓 = 𝐹 → seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝑓 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 ) ) ) = seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) )
11 elex ⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
12 seqex ⊢ seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ∈ V
13 12 a1i ⊢ ( 𝐹 ∈ 𝑉 → seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ∈ V )
14 1 10 11 13 fvmptd3 ⊢ ( 𝐹 ∈ 𝑉 → ( IterComp ‘ 𝐹 ) = seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) )