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	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to IterComp (F) (Y + 1) = F \circ G$

Proof

Step	Hyp	Ref	Expression
1		itcovalsuc	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to IterComp (F) (Y + 1) = G (g \in V, j \in V ⟼ F \circ g) F$
2		eqidd	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to (g \in V, j \in V ⟼ F \circ g) = (g \in V, j \in V ⟼ F \circ g)$
3		coeq2	$⊢ g = G \to F \circ g = F \circ G$
4	3	ad2antrl	$⊢ ((F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \land (g = G \land j = F)) \to F \circ g = F \circ G$
5		id	$⊢ G = IterComp (F) (Y) \to G = IterComp (F) (Y)$
6		fvex	$⊢ IterComp (F) (Y) \in V$
7	5 6	eqeltrdi	$⊢ G = IterComp (F) (Y) \to G \in V$
8	7	eqcoms	$⊢ IterComp (F) (Y) = G \to G \in V$
9	8	3ad2ant3	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to G \in V$
10		elex	$⊢ F \in V \to F \in V$
11	10	3ad2ant1	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to F \in V$
12	8	anim2i	$⊢ (F \in V \land IterComp (F) (Y) = G) \to (F \in V \land G \in V)$
13	12	3adant2	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to (F \in V \land G \in V)$
14		coexg	$⊢ (F \in V \land G \in V) \to F \circ G \in V$
15	13 14	syl	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to F \circ G \in V$
16	2 4 9 11 15	ovmpod	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to G (g \in V, j \in V ⟼ F \circ g) F = F \circ G$
17	1 16	eqtrd	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to IterComp (F) (Y + 1) = F \circ G$