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

Metamath Proof Explorer

Theorem imaidfu2lem

Description: Lemma for imaidfu2 . (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses imaidfu.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
imaidfu.d ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 Func 𝐸 ) )
Assertion imaidfu2lem ( 𝜑 → ( ( 1st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 imaidfu.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
2 imaidfu.d ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 Func 𝐸 ) )
3 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) )
4 1 2 3 idfu1sta ⊢ ( 𝜑 → ( 1st ‘ 𝐼 ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
5 4 imaeq1d ⊢ ( 𝜑 → ( ( 1st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( ( I ↾ ( Base ‘ 𝐷 ) ) “ ( Base ‘ 𝐷 ) ) )
6 ssid ⊢ ( Base ‘ 𝐷 ) ⊆ ( Base ‘ 𝐷 )
7 resiima ⊢ ( ( Base ‘ 𝐷 ) ⊆ ( Base ‘ 𝐷 ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) “ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 ) )
8 6 7 ax-mp ⊢ ( ( I ↾ ( Base ‘ 𝐷 ) ) “ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 )
9 5 8 eqtrdi ⊢ ( 𝜑 → ( ( 1st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 ) )