Theorem cofid2a

Description: Express the morphism 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 )
	cofid2a.y	|- ( ph -> Y e. B )
	cofid2a.h	|- H = ( Hom ` D )
	cofid2a.r	|- ( ph -> R e. ( X H Y ) )
Assertion	cofid2a	|- ( ph -> ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) = R )

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		cofid2a.y	|- ( ph -> Y e. B )
8		cofid2a.h	|- H = ( Hom ` D )
9		cofid2a.r	|- ( ph -> R e. ( X H Y ) )
10	6	fveq2d	|- ( ph -> ( 2nd ` ( G o.func F ) ) = ( 2nd ` I ) )
11	10	oveqd	|- ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( X ( 2nd ` I ) Y ) )
12	11	fveq1d	|- ( ph -> ( ( X ( 2nd ` ( G o.func F ) ) Y ) ` R ) = ( ( X ( 2nd ` I ) Y ) ` R ) )
13	2 4 5 3 7 8 9	cofu2	|- ( ph -> ( ( X ( 2nd ` ( G o.func F ) ) Y ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) )
14	4	func1st2nd	|- ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
15	14	funcrcl2	|- ( ph -> D e. Cat )
16	1 2 15 8 3 7 9	idfu2	|- ( ph -> ( ( X ( 2nd ` I ) Y ) ` R ) = R )
17	12 13 16	3eqtr3d	|- ( ph -> ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) = R )