Theorem idfu1stalem

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

	Ref	Expression
Hypotheses	idfu2nda.i	|- I = ( idFunc ` C )
	idfu2nda.d	|- ( ph -> I e. ( D Func E ) )
	idfu2nda.b	|- ( ph -> B = ( Base ` D ) )
Assertion	idfu1stalem	|- ( ph -> B = ( Base ` C ) )

Proof

Step	Hyp	Ref	Expression
1		idfu2nda.i	|- I = ( idFunc ` C )
2		idfu2nda.d	|- ( ph -> I e. ( D Func E ) )
3		idfu2nda.b	|- ( ph -> B = ( Base ` D ) )
4	1 2	eqeltrrid	|- ( ph -> ( idFunc ` C ) e. ( D Func E ) )
5		idfurcl	|- ( ( idFunc ` C ) e. ( D Func E ) -> C e. Cat )
6	1	idfucl	|- ( C e. Cat -> I e. ( C Func C ) )
7	4 5 6	3syl	|- ( ph -> I e. ( C Func C ) )
8	7	func1st2nd	|- ( ph -> ( 1st ` I ) ( C Func C ) ( 2nd ` I ) )
9	2	func1st2nd	|- ( ph -> ( 1st ` I ) ( D Func E ) ( 2nd ` I ) )
10	8 9	funchomf	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
11	10	homfeqbas	|- ( ph -> ( Base ` C ) = ( Base ` D ) )
12	3 11	eqtr4d	|- ( ph -> B = ( Base ` C ) )