Theorem idfu1stalem

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

	Ref	Expression
Hypotheses	idfu2nda.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	idfu2nda.d	$$⊢\phi \to I\in \left(D\mathrm{Func}E\right)$$
	idfu2nda.b	$$⊢\phi \to B={\mathrm{Base}}_D$$
Assertion	idfu1stalem	$$⊢\phi \to B={\mathrm{Base}}_C$$

Proof

Step	Hyp	Ref	Expression
1		idfu2nda.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
2		idfu2nda.d	$$⊢\phi \to I\in \left(D\mathrm{Func}E\right)$$
3		idfu2nda.b	$$⊢\phi \to B={\mathrm{Base}}_D$$
4	1 2	eqeltrrid	$$⊢\phi \to {id}_{\mathrm{func}}\left(C\right)\in \left(D\mathrm{Func}E\right)$$
5		idfurcl	$$⊢{id}_{\mathrm{func}}\left(C\right)\in \left(D\mathrm{Func}E\right)\to C\in \mathrm{Cat}$$
6	1	idfucl	$$⊢C\in \mathrm{Cat}\to I\in \left(C\mathrm{Func}C\right)$$
7	4 5 6	3syl	$$⊢\phi \to I\in \left(C\mathrm{Func}C\right)$$
8	7	func1st2nd	$$⊢\phi \to 1^{st}\left(I\right)\left(C\mathrm{Func}C\right)2^{nd}\left(I\right)$$
9	2	func1st2nd	$$⊢\phi \to 1^{st}\left(I\right)\left(D\mathrm{Func}E\right)2^{nd}\left(I\right)$$
10	8 9	funchomf	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
11	10	homfeqbas	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_D$$
12	3 11	eqtr4d	$$⊢\phi \to B={\mathrm{Base}}_C$$