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 e. A |-> B )
Assertion itcoval0mpt 
|- ( ( A e. V /\ A. n e. A B e. W ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. A |-> n ) )

Proof

Step Hyp Ref Expression
1 itcoval0mpt.f 
 |-  F = ( n e. A |-> B )
2 1 fveq2i 
 |-  ( IterComp ` F ) = ( IterComp ` ( n e. A |-> B ) )
3 2 fveq1i 
 |-  ( ( IterComp ` F ) ` 0 ) = ( ( IterComp ` ( n e. A |-> B ) ) ` 0 )
4 mptexg 
 |-  ( A e. V -> ( n e. A |-> B ) e. _V )
5 itcoval0 
 |-  ( ( n e. A |-> B ) e. _V -> ( ( IterComp ` ( n e. A |-> B ) ) ` 0 ) = ( _I |` dom ( n e. A |-> B ) ) )
6 4 5 syl 
 |-  ( A e. V -> ( ( IterComp ` ( n e. A |-> B ) ) ` 0 ) = ( _I |` dom ( n e. A |-> B ) ) )
7 3 6 syl5eq 
 |-  ( A e. V -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom ( n e. A |-> B ) ) )
8 dmmptg 
 |-  ( A. n e. A B e. W -> dom ( n e. A |-> B ) = A )
9 8 reseq2d 
 |-  ( A. n e. A B e. W -> ( _I |` dom ( n e. A |-> B ) ) = ( _I |` A ) )
10 mptresid 
 |-  ( _I |` A ) = ( n e. A |-> n )
11 9 10 eqtrdi 
 |-  ( A. n e. A B e. W -> ( _I |` dom ( n e. A |-> B ) ) = ( n e. A |-> n ) )
12 7 11 sylan9eq 
 |-  ( ( A e. V /\ A. n e. A B e. W ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. A |-> n ) )