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 𝐹 = ( 𝑛𝐴𝐵 )
Assertion itcoval0mpt ( ( 𝐴𝑉 ∧ ∀ 𝑛𝐴 𝐵𝑊 ) → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛𝐴𝑛 ) )

Proof

Step Hyp Ref Expression
1 itcoval0mpt.f 𝐹 = ( 𝑛𝐴𝐵 )
2 1 fveq2i ( IterComp ‘ 𝐹 ) = ( IterComp ‘ ( 𝑛𝐴𝐵 ) )
3 2 fveq1i ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( ( IterComp ‘ ( 𝑛𝐴𝐵 ) ) ‘ 0 )
4 mptexg ( 𝐴𝑉 → ( 𝑛𝐴𝐵 ) ∈ V )
5 itcoval0 ( ( 𝑛𝐴𝐵 ) ∈ V → ( ( IterComp ‘ ( 𝑛𝐴𝐵 ) ) ‘ 0 ) = ( I ↾ dom ( 𝑛𝐴𝐵 ) ) )
6 4 5 syl ( 𝐴𝑉 → ( ( IterComp ‘ ( 𝑛𝐴𝐵 ) ) ‘ 0 ) = ( I ↾ dom ( 𝑛𝐴𝐵 ) ) )
7 3 6 syl5eq ( 𝐴𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( I ↾ dom ( 𝑛𝐴𝐵 ) ) )
8 dmmptg ( ∀ 𝑛𝐴 𝐵𝑊 → dom ( 𝑛𝐴𝐵 ) = 𝐴 )
9 8 reseq2d ( ∀ 𝑛𝐴 𝐵𝑊 → ( I ↾ dom ( 𝑛𝐴𝐵 ) ) = ( I ↾ 𝐴 ) )
10 mptresid ( I ↾ 𝐴 ) = ( 𝑛𝐴𝑛 )
11 9 10 eqtrdi ( ∀ 𝑛𝐴 𝐵𝑊 → ( I ↾ dom ( 𝑛𝐴𝐵 ) ) = ( 𝑛𝐴𝑛 ) )
12 7 11 sylan9eq ( ( 𝐴𝑉 ∧ ∀ 𝑛𝐴 𝐵𝑊 ) → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛𝐴𝑛 ) )