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 ) = ( 𝑛 ∈ 𝐴 ↦ 𝑛 ) )