Theorem cofid1

Description: Express the object part of ( G o.func F ) = I explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

	Ref	Expression
Hypotheses	cofid1a.i	|- I = ( idFunc ` D )
	cofid1a.b	|- B = ( Base ` D )
	cofid1a.x	|- ( ph -> X e. B )
	cofid1.f	|- ( ph -> F ( D Func E ) G )
	cofid1.k	|- ( ph -> K ( E Func D ) L )
	cofid1.o	|- ( ph -> ( <. K , L >. o.func <. F , G >. ) = I )
Assertion	cofid1	|- ( ph -> ( K ` ( F ` X ) ) = X )

Proof

Step	Hyp	Ref	Expression
1		cofid1a.i	|- I = ( idFunc ` D )
2		cofid1a.b	|- B = ( Base ` D )
3		cofid1a.x	|- ( ph -> X e. B )
4		cofid1.f	|- ( ph -> F ( D Func E ) G )
5		cofid1.k	|- ( ph -> K ( E Func D ) L )
6		cofid1.o	|- ( ph -> ( <. K , L >. o.func <. F , G >. ) = I )
7	5	func1st	|- ( ph -> ( 1st ` <. K , L >. ) = K )
8	4	func1st	|- ( ph -> ( 1st ` <. F , G >. ) = F )
9	8	fveq1d	|- ( ph -> ( ( 1st ` <. F , G >. ) ` X ) = ( F ` X ) )
10	7 9	fveq12d	|- ( ph -> ( ( 1st ` <. K , L >. ) ` ( ( 1st ` <. F , G >. ) ` X ) ) = ( K ` ( F ` X ) ) )
11		df-br	|- ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) )
12	4 11	sylib	|- ( ph -> <. F , G >. e. ( D Func E ) )
13		df-br	|- ( K ( E Func D ) L <-> <. K , L >. e. ( E Func D ) )
14	5 13	sylib	|- ( ph -> <. K , L >. e. ( E Func D ) )
15	1 2 3 12 14 6	cofid1a	|- ( ph -> ( ( 1st ` <. K , L >. ) ` ( ( 1st ` <. F , G >. ) ` X ) ) = X )
16	10 15	eqtr3d	|- ( ph -> ( K ` ( F ` X ) ) = X )