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

Metamath Proof Explorer

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 )