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

Metamath Proof Explorer

Theorem cofidvala

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

Ref Expression
Hypotheses cofidvala.i 
|- I = ( idFunc ` D )
cofidvala.b 
|- B = ( Base ` D )
cofidvala.f 
|- ( ph -> F e. ( D Func E ) )
cofidvala.g 
|- ( ph -> G e. ( E Func D ) )
cofidvala.o 
|- ( ph -> ( G o.func F ) = I )
cofidvala.h 
|- H = ( Hom ` D )
Assertion cofidvala 
|- ( ph -> ( ( ( 1st ` G ) o. ( 1st ` F ) ) = ( _I |` B ) /\ ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) ) )

Proof

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