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