Metamath Proof Explorer

Theorem itcovalendof

Description: The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024)

Ref Expression
Hypotheses itcovalendof.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
itcovalendof.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐴 )
itcovalendof.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion itcovalendof ( 𝜑 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑁 ) : 𝐴 ⟶ 𝐴 )

Proof

Step Hyp Ref Expression
1 itcovalendof.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 itcovalendof.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐴 )
3 itcovalendof.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 fveq2 ⊢ ( 𝑥 = 0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 0 ) )
5 4 feq1d ⊢ ( 𝑥 = 0 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) : 𝐴 ⟶ 𝐴 ↔ ( ( IterComp ‘ 𝐹 ) ‘ 0 ) : 𝐴 ⟶ 𝐴 ) )
6 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) )
7 6 feq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) : 𝐴 ⟶ 𝐴 ↔ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) )
8 fveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) )
9 8 feq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) : 𝐴 ⟶ 𝐴 ↔ ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) : 𝐴 ⟶ 𝐴 ) )
10 fveq2 ⊢ ( 𝑥 = 𝑁 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝑁 ) )
11 10 feq1d ⊢ ( 𝑥 = 𝑁 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) : 𝐴 ⟶ 𝐴 ↔ ( ( IterComp ‘ 𝐹 ) ‘ 𝑁 ) : 𝐴 ⟶ 𝐴 ) )
12 f1oi ⊢ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴
13 f1of ⊢ ( ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴 → ( I ↾ 𝐴 ) : 𝐴 ⟶ 𝐴 )
14 12 13 mp1i ⊢ ( 𝜑 → ( I ↾ 𝐴 ) : 𝐴 ⟶ 𝐴 )
15 2 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
16 15 reseq2d ⊢ ( 𝜑 → ( I ↾ dom 𝐹 ) = ( I ↾ 𝐴 ) )
17 16 feq1d ⊢ ( 𝜑 → ( ( I ↾ dom 𝐹 ) : 𝐴 ⟶ 𝐴 ↔ ( I ↾ 𝐴 ) : 𝐴 ⟶ 𝐴 ) )
18 14 17 mpbird ⊢ ( 𝜑 → ( I ↾ dom 𝐹 ) : 𝐴 ⟶ 𝐴 )
19 2 1 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
20 itcoval0 ⊢ ( 𝐹 ∈ V → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( I ↾ dom 𝐹 ) )
21 19 20 syl ⊢ ( 𝜑 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( I ↾ dom 𝐹 ) )
22 21 feq1d ⊢ ( 𝜑 → ( ( ( IterComp ‘ 𝐹 ) ‘ 0 ) : 𝐴 ⟶ 𝐴 ↔ ( I ↾ dom 𝐹 ) : 𝐴 ⟶ 𝐴 ) )
23 18 22 mpbird ⊢ ( 𝜑 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) : 𝐴 ⟶ 𝐴 )
24 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐴 )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 )
26 24 25 fcod ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) → ( 𝐹 ∘ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) ) : 𝐴 ⟶ 𝐴 )
27 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) → 𝐹 ∈ V )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) → 𝑦 ∈ ℕ0 )
29 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) )
30 itcovalsucov ⊢ ( ( 𝐹 ∈ V ∧ 𝑦 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ∘ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) ) )
31 27 28 29 30 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ∘ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) ) )
32 31 feq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) : 𝐴 ⟶ 𝐴 ↔ ( 𝐹 ∘ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) ) : 𝐴 ⟶ 𝐴 ) )
33 26 32 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) : 𝐴 ⟶ 𝐴 ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) : 𝐴 ⟶ 𝐴 )
34 5 7 9 11 23 33 nn0indd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑁 ) : 𝐴 ⟶ 𝐴 )
35 3 34 mpdan ⊢ ( 𝜑 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑁 ) : 𝐴 ⟶ 𝐴 )