Metamath Proof Explorer

Theorem cofidval

Description: The property " <. F , G >. is a section of <. K , L >. " in a category of small categories (in a universe); expressed explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Hypotheses cofidval.i 
|- I = ( idFunc ` D )
cofidval.b 
|- B = ( Base ` D )
cofidval.f 
|- ( ph -> F ( D Func E ) G )
cofidval.k 
|- ( ph -> K ( E Func D ) L )
cofidval.o 
|- ( ph -> ( <. K , L >. o.func <. F , G >. ) = I )
cofidval.h 
|- H = ( Hom ` D )
Assertion cofidval 
|- ( ph -> ( ( K o. F ) = ( _I |` B ) /\ ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cofidval.i 
 |-  I = ( idFunc ` D )
2 cofidval.b 
 |-  B = ( Base ` D )
3 cofidval.f 
 |-  ( ph -> F ( D Func E ) G )
4 cofidval.k 
 |-  ( ph -> K ( E Func D ) L )
5 cofidval.o 
 |-  ( ph -> ( <. K , L >. o.func <. F , G >. ) = I )
6 cofidval.h 
 |-  H = ( Hom ` D )
7 2 3 4 cofuval2 
 |-  ( ph -> ( <. K , L >. o.func <. F , G >. ) = <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. )
8 3 funcrcl2 
 |-  ( ph -> D e. Cat )
9 1 2 8 6 idfuval 
 |-  ( ph -> I = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
10 5 7 9 3eqtr3d 
 |-  ( ph -> <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
11 2 fvexi 
 |-  B e. _V
12 resiexg 
 |-  ( B e. _V -> ( _I |` B ) e. _V )
13 11 12 ax-mp 
 |-  ( _I |` B ) e. _V
14 11 11 xpex 
 |-  ( B X. B ) e. _V
15 14 mptex 
 |-  ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) e. _V
16 13 15 opth2 
 |-  ( <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. <-> ( ( K o. F ) = ( _I |` B ) /\ ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) ) )
17 10 16 sylib 
 |-  ( ph -> ( ( K o. F ) = ( _I |` B ) /\ ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) ) )