Theorem itcovalsucov

Description: The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024)

	Ref	Expression
Assertion	itcovalsucov	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑌 + 1 ) ) = ( 𝐹 ∘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		itcovalsuc	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑌 + 1 ) ) = ( 𝐺 ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) )
2		eqidd	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) = ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) )
3		coeq2	⊢ ( 𝑔 = 𝐺 → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ 𝐺 ) )
4	3	ad2antrl	⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) ∧ ( 𝑔 = 𝐺 ∧ 𝑗 = 𝐹 ) ) → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ 𝐺 ) )
5		id	⊢ ( 𝐺 = ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) → 𝐺 = ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) )
6		fvex	⊢ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) ∈ V
7	5 6	eqeltrdi	⊢ ( 𝐺 = ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) → 𝐺 ∈ V )
8	7	eqcoms	⊢ ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 → 𝐺 ∈ V )
9	8	3ad2ant3	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → 𝐺 ∈ V )
10		elex	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
11	10	3ad2ant1	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → 𝐹 ∈ V )
12	8	anim2i	⊢ ( ( 𝐹 ∈ 𝑉 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ V ) )
13	12	3adant2	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ V ) )
14		coexg	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ V ) → ( 𝐹 ∘ 𝐺 ) ∈ V )
15	13 14	syl	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( 𝐹 ∘ 𝐺 ) ∈ V )
16	2 4 9 11 15	ovmpod	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( 𝐺 ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) = ( 𝐹 ∘ 𝐺 ) )
17	1 16	eqtrd	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑌 + 1 ) ) = ( 𝐹 ∘ 𝐺 ) )