Metamath Proof Explorer


Theorem itcoval0mpt

Description: A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024)

Ref Expression
Hypothesis itcoval0mpt.f F = n A B
Assertion itcoval0mpt A V n A B W IterComp F 0 = n A n

Proof

Step Hyp Ref Expression
1 itcoval0mpt.f F = n A B
2 1 fveq2i IterComp F = IterComp n A B
3 2 fveq1i IterComp F 0 = IterComp n A B 0
4 mptexg A V n A B V
5 itcoval0 n A B V IterComp n A B 0 = I dom n A B
6 4 5 syl A V IterComp n A B 0 = I dom n A B
7 3 6 eqtrid A V IterComp F 0 = I dom n A B
8 dmmptg n A B W dom n A B = A
9 8 reseq2d n A B W I dom n A B = I A
10 mptresid I A = n A n
11 9 10 eqtrdi n A B W I dom n A B = n A n
12 7 11 sylan9eq A V n A B W IterComp F 0 = n A n