This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) = ( 𝐹 ∘ 𝐺 ) )