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 ‘ 𝐹 ) ‘ 𝑁 ) : 𝐴𝐴 )