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 = f ∈ V ⟼ seq 0 g ∈ V , j ∈ V ⟼ f ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ f f

Detailed syntax breakdown

Step Hyp Ref Expression
0 citco class IterComp
1 vf setvar f
2 cvv class V
3 cc0 class 0
4 vg setvar g
5 vj setvar j
6 1 cv setvar f
7 4 cv setvar g
8 6 7 ccom class f ∘ g
9 4 5 2 2 8 cmpo class g ∈ V , j ∈ V ⟼ f ∘ g
10 vi setvar i
11 cn0 class ℕ 0
12 10 cv setvar i
13 12 3 wceq wff i = 0
14 cid class I
15 6 cdm class dom ⁡ f
16 14 15 cres class I ↾ dom ⁡ f
17 13 16 6 cif class if i = 0 I ↾ dom ⁡ f f
18 10 11 17 cmpt class i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ f f
19 9 18 3 cseq class seq 0 g ∈ V , j ∈ V ⟼ f ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ f f
20 1 2 19 cmpt class f ∈ V ⟼ seq 0 g ∈ V , j ∈ V ⟼ f ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ f f
21 0 20 wceq wff IterComp = f ∈ V ⟼ seq 0 g ∈ V , j ∈ V ⟼ f ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ f f