Theorem cofid1a

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 )
	cofid1a.f	|- ( ph -> F e. ( D Func E ) )
	cofid1a.g	|- ( ph -> G e. ( E Func D ) )
	cofid1a.o	|- ( ph -> ( G o.func F ) = I )
Assertion	cofid1a	|- ( ph -> ( ( 1st ` G ) ` ( ( 1st ` 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		cofid1a.f	|- ( ph -> F e. ( D Func E ) )
5		cofid1a.g	|- ( ph -> G e. ( E Func D ) )
6		cofid1a.o	|- ( ph -> ( G o.func F ) = I )
7	6	fveq2d	|- ( ph -> ( 1st ` ( G o.func F ) ) = ( 1st ` I ) )
8	7	fveq1d	|- ( ph -> ( ( 1st ` ( G o.func F ) ) ` X ) = ( ( 1st ` I ) ` X ) )
9	2 4 5 3	cofu1	|- ( ph -> ( ( 1st ` ( G o.func F ) ) ` X ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) )
10	4	func1st2nd	|- ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
11	10	funcrcl2	|- ( ph -> D e. Cat )
12	1 2 11 3	idfu1	|- ( ph -> ( ( 1st ` I ) ` X ) = X )
13	8 9 12	3eqtr3d	|- ( ph -> ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) = X )