Theorem imaidfu2lem

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

	Ref	Expression
Hypotheses	imaidfu.i	|- I = ( idFunc ` C )
	imaidfu.d	|- ( ph -> I e. ( D Func E ) )
Assertion	imaidfu2lem	|- ( ph -> ( ( 1st ` I ) " ( Base ` D ) ) = ( Base ` D ) )

Proof

Step	Hyp	Ref	Expression
1		imaidfu.i	|- I = ( idFunc ` C )
2		imaidfu.d	|- ( ph -> I e. ( D Func E ) )
3		eqidd	|- ( ph -> ( Base ` D ) = ( Base ` D ) )
4	1 2 3	idfu1sta	|- ( ph -> ( 1st ` I ) = ( _I |` ( Base ` D ) ) )
5	4	imaeq1d	|- ( ph -> ( ( 1st ` I ) " ( Base ` D ) ) = ( ( _I |` ( Base ` D ) ) " ( Base ` D ) ) )
6		ssid	|- ( Base ` D ) C_ ( Base ` D )
7		resiima	|- ( ( Base ` D ) C_ ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) " ( Base ` D ) ) = ( Base ` D ) )
8	6 7	ax-mp	|- ( ( _I |` ( Base ` D ) ) " ( Base ` D ) ) = ( Base ` D )
9	5 8	eqtrdi	|- ( ph -> ( ( 1st ` I ) " ( Base ` D ) ) = ( Base ` D ) )