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 φ A V
itcovalendof.f φ F : A A
itcovalendof.n φ N 0
Assertion itcovalendof φ IterComp F N : A A

Proof

Step Hyp Ref Expression
1 itcovalendof.a φ A V
2 itcovalendof.f φ F : A A
3 itcovalendof.n φ N 0
4 fveq2 x = 0 IterComp F x = IterComp F 0
5 4 feq1d x = 0 IterComp F x : A A IterComp F 0 : A A
6 fveq2 x = y IterComp F x = IterComp F y
7 6 feq1d x = y IterComp F x : A A IterComp F y : A A
8 fveq2 x = y + 1 IterComp F x = IterComp F y + 1
9 8 feq1d x = y + 1 IterComp F x : A A IterComp F y + 1 : A A
10 fveq2 x = N IterComp F x = IterComp F N
11 10 feq1d x = N IterComp F x : A A IterComp F N : A A
12 f1oi I A : A 1-1 onto A
13 f1of I A : A 1-1 onto A I A : A A
14 12 13 mp1i φ I A : A A
15 2 fdmd φ dom F = A
16 15 reseq2d φ I dom F = I A
17 16 feq1d φ I dom F : A A I A : A A
18 14 17 mpbird φ I dom F : A A
19 2 1 fexd φ F V
20 itcoval0 F V IterComp F 0 = I dom F
21 19 20 syl φ IterComp F 0 = I dom F
22 21 feq1d φ IterComp F 0 : A A I dom F : A A
23 18 22 mpbird φ IterComp F 0 : A A
24 2 ad2antrr φ y 0 IterComp F y : A A F : A A
25 simpr φ y 0 IterComp F y : A A IterComp F y : A A
26 24 25 fcod φ y 0 IterComp F y : A A F IterComp F y : A A
27 19 ad2antrr φ y 0 IterComp F y : A A F V
28 simplr φ y 0 IterComp F y : A A y 0
29 eqidd φ y 0 IterComp F y : A A IterComp F y = IterComp F y
30 itcovalsucov F V y 0 IterComp F y = IterComp F y IterComp F y + 1 = F IterComp F y
31 27 28 29 30 syl3anc φ y 0 IterComp F y : A A IterComp F y + 1 = F IterComp F y
32 31 feq1d φ y 0 IterComp F y : A A IterComp F y + 1 : A A F IterComp F y : A A
33 26 32 mpbird φ y 0 IterComp F y : A A IterComp F y + 1 : A A
34 5 7 9 11 23 33 nn0indd φ N 0 IterComp F N : A A
35 3 34 mpdan φ IterComp F N : A A