Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-itco Structured version   Visualization version   GIF version

Definition df-itco 45087
 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.)
Assertion
Ref Expression
df-itco IterComp = (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))))
Distinct variable group:   𝑓,𝑔,𝑖,𝑗

Detailed syntax breakdown of Definition df-itco
StepHypRef Expression
1 citco 45085 . 2 class IterComp
2 vf . . 3 setvar 𝑓
3 cvv 3441 . . 3 class V
4 vg . . . . 5 setvar 𝑔
5 vj . . . . 5 setvar 𝑗
62cv 1537 . . . . . 6 class 𝑓
74cv 1537 . . . . . 6 class 𝑔
86, 7ccom 5523 . . . . 5 class (𝑓𝑔)
94, 5, 3, 3, 8cmpo 7137 . . . 4 class (𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓𝑔))
10 vi . . . . 5 setvar 𝑖
11 cn0 11887 . . . . 5 class 0
1210cv 1537 . . . . . . 7 class 𝑖
13 cc0 10528 . . . . . . 7 class 0
1412, 13wceq 1538 . . . . . 6 wff 𝑖 = 0
15 cid 5424 . . . . . . 7 class I
166cdm 5519 . . . . . . 7 class dom 𝑓
1715, 16cres 5521 . . . . . 6 class ( I ↾ dom 𝑓)
1814, 17, 6cif 4425 . . . . 5 class if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓)
1910, 11, 18cmpt 5110 . . . 4 class (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))
209, 19, 13cseq 13366 . . 3 class seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓)))
212, 3, 20cmpt 5110 . 2 class (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))))
221, 21wceq 1538 1 wff IterComp = (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))))
 Colors of variables: wff setvar class This definition is referenced by:  itcoval  45089
 Copyright terms: Public domain W3C validator