Theorem cofu1stfix

Description: Post-composition by an object-fixing functor preserves the entire object function, including its exact domain. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	cofu1stfix.a	|- A = ( Base ` E )
	cofu1stfix.f	|- ( ph -> F e. ( D Func E ) )
	cofu1stfix.k	|- ( ph -> K e. ( E Func E ) )
	cofu1stfix.i	|- ( ph -> ( 1st ` K ) = ( _I |` A ) )
Assertion	cofu1stfix	|- ( ph -> ( 1st ` ( K o.func F ) ) = ( 1st ` F ) )

Proof

Step	Hyp	Ref	Expression
1		cofu1stfix.a	|- A = ( Base ` E )
2		cofu1stfix.f	|- ( ph -> F e. ( D Func E ) )
3		cofu1stfix.k	|- ( ph -> K e. ( E Func E ) )
4		cofu1stfix.i	|- ( ph -> ( 1st ` K ) = ( _I |` A ) )
5		eqid	|- ( Base ` D ) = ( Base ` D )
6	5 2 3	cofu1st	|- ( ph -> ( 1st ` ( K o.func F ) ) = ( ( 1st ` K ) o. ( 1st ` F ) ) )
7	4	coeq1d	|- ( ph -> ( ( 1st ` K ) o. ( 1st ` F ) ) = ( ( _I |` A ) o. ( 1st ` F ) ) )
8	2	func1st2nd	|- ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
9	5 1 8	funcf1	|- ( ph -> ( 1st ` F ) : ( Base ` D ) --> A )
10		fcoi2	|- ( ( 1st ` F ) : ( Base ` D ) --> A -> ( ( _I |` A ) o. ( 1st ` F ) ) = ( 1st ` F ) )
11	9 10	syl	|- ( ph -> ( ( _I |` A ) o. ( 1st ` F ) ) = ( 1st ` F ) )
12	6 7 11	3eqtrd	|- ( ph -> ( 1st ` ( K o.func F ) ) = ( 1st ` F ) )