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

Metamath Proof Explorer

Definition df-itco

Description: Define a function (recursively) that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 2-May-2024)

Ref Expression
Assertion df-itco IterComp = ( 𝑓 ∈ V ↦ seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝑓 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 citco ⊢ IterComp
1 vf ⊢ 𝑓
2 cvv ⊢ V
3 cc0 ⊢ 0
4 vg ⊢ 𝑔
5 vj ⊢ 𝑗
6 1 cv ⊢ 𝑓
7 4 cv ⊢ 𝑔
8 6 7 ccom ⊢ ( 𝑓 ∘ 𝑔 )
9 4 5 2 2 8 cmpo ⊢ ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝑓 ∘ 𝑔 ) )
10 vi ⊢ 𝑖
11 cn0 ⊢ ℕ0
12 10 cv ⊢ 𝑖
13 12 3 wceq ⊢ 𝑖 = 0
14 cid ⊢ I
15 6 cdm ⊢ dom 𝑓
16 14 15 cres ⊢ ( I ↾ dom 𝑓 )
17 13 16 6 cif ⊢ if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 )
18 10 11 17 cmpt ⊢ ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 ) )
19 9 18 3 cseq ⊢ seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝑓 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 ) ) )
20 1 2 19 cmpt ⊢ ( 𝑓 ∈ V ↦ seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝑓 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 ) ) ) )
21 0 20 wceq ⊢ IterComp = ( 𝑓 ∈ V ↦ seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝑓 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝑓 ) , 𝑓 ) ) ) )