This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ( ( 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 ) = ( 𝑛 ∈ 𝐴 ↦ 𝑛 ) )