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 ‘ 𝐷 ) )