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

Metamath Proof Explorer

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 )