Metamath Proof Explorer

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 ⊢ F ∈ V → IterComp ⁡ F = seq 0 g ∈ V , j ∈ V ⟼ F ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F

Proof

Step Hyp Ref Expression
1 df-itco ⊢ IterComp = f ∈ V ⟼ seq 0 g ∈ V , j ∈ V ⟼ f ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ f f
2 eqidd ⊢ f = F → 0 = 0
3 coeq1 ⊢ f = F → f ∘ g = F ∘ g
4 3 mpoeq3dv ⊢ f = F → g ∈ V , j ∈ V ⟼ f ∘ g = g ∈ V , j ∈ V ⟼ F ∘ g
5 dmeq ⊢ f = F → dom ⁡ f = dom ⁡ F
6 5 reseq2d ⊢ f = F → I ↾ dom ⁡ f = I ↾ dom ⁡ F
7 id ⊢ f = F → f = F
8 6 7 ifeq12d ⊢ f = F → if i = 0 I ↾ dom ⁡ f f = if i = 0 I ↾ dom ⁡ F F
9 8 mpteq2dv ⊢ f = F → i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ f f = i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F
10 2 4 9 seqeq123d ⊢ f = F → seq 0 g ∈ V , j ∈ V ⟼ f ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ f f = seq 0 g ∈ V , j ∈ V ⟼ F ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F
11 elex ⊢ F ∈ V → F ∈ V
12 seqex ⊢ seq 0 g ∈ V , j ∈ V ⟼ F ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F ∈ V
13 12 a1i ⊢ F ∈ V → seq 0 g ∈ V , j ∈ V ⟼ F ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F ∈ V
14 1 10 11 13 fvmptd3 ⊢ F ∈ V → IterComp ⁡ F = seq 0 g ∈ V , j ∈ V ⟼ F ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F