Theorem imaidfu2lem

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

	Ref	Expression
Hypotheses	imaidfu.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	imaidfu.d	$$⊢\phi \to I\in \left(D\mathrm{Func}E\right)$$
Assertion	imaidfu2lem	$$⊢\phi \to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D$$

Proof

Step	Hyp	Ref	Expression
1		imaidfu.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
2		imaidfu.d	$$⊢\phi \to I\in \left(D\mathrm{Func}E\right)$$
3		eqidd	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_D$$
4	1 2 3	idfu1sta	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}$$
5	4	imaeq1d	$$⊢\phi \to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]=\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)\left[{\mathrm{Base}}_D\right]$$
6		ssid	$$⊢{\mathrm{Base}}_D\subseteq {\mathrm{Base}}_D$$
7		resiima	$$⊢{\mathrm{Base}}_D\subseteq {\mathrm{Base}}_D\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D$$
8	6 7	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D$$
9	5 8	eqtrdi	$$⊢\phi \to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D$$