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