This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )