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 𝑓 ) , 𝑓 ) ) ) )