Metamath Proof Explorer

Theorem cofidf2a

Description: If " F is a section of G " in a category of small categories (in a universe), then the morphism part of F is injective, and the morphism part of G is surjective in the image of F . (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 )
cofidf2a.j 
|- J = ( Hom ` E )
cofidf2a.x 
|- ( ph -> X e. B )
cofidf2a.y 
|- ( ph -> Y e. B )
Assertion cofidf2a 
|- ( ph -> ( ( X ( 2nd ` F ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) /\ ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) : ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) -onto-> ( X H Y ) ) )

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 cofidf2a.j 
 |-  J = ( Hom ` E )
8 cofidf2a.x 
 |-  ( ph -> X e. B )
9 cofidf2a.y 
 |-  ( ph -> Y e. B )
10 3 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
11 2 6 7 10 8 9 funcf2 
 |-  ( ph -> ( X ( 2nd ` F ) Y ) : ( X H Y ) --> ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) )
12 5 fveq2d 
 |-  ( ph -> ( 2nd ` ( G o.func F ) ) = ( 2nd ` I ) )
13 12 oveqd 
 |-  ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( X ( 2nd ` I ) Y ) )
14 2 3 4 8 9 cofu2nd 
 |-  ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) )
15 10 funcrcl2 
 |-  ( ph -> D e. Cat )
16 1 2 15 6 8 9 idfu2nd 
 |-  ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` ( X H Y ) ) )
17 13 14 16 3eqtr3d 
 |-  ( ph -> ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) = ( _I |` ( X H Y ) ) )
18 fcof1 
 |-  ( ( ( X ( 2nd ` F ) Y ) : ( X H Y ) --> ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) /\ ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) = ( _I |` ( X H Y ) ) ) -> ( X ( 2nd ` F ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) )
19 11 17 18 syl2anc 
 |-  ( ph -> ( X ( 2nd ` F ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) )
20 1 2 8 3 4 5 cofid1a 
 |-  ( ph -> ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) = X )
21 1 2 9 3 4 5 cofid1a 
 |-  ( ph -> ( ( 1st ` G ) ` ( ( 1st ` F ) ` Y ) ) = Y )
22 20 21 oveq12d 
 |-  ( ph -> ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) H ( ( 1st ` G ) ` ( ( 1st ` F ) ` Y ) ) ) = ( X H Y ) )
23 eqid 
 |-  ( Base ` E ) = ( Base ` E )
24 4 func1st2nd 
 |-  ( ph -> ( 1st ` G ) ( E Func D ) ( 2nd ` G ) )
25 2 23 10 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` E ) )
26 25 8 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` F ) ` X ) e. ( Base ` E ) )
27 25 9 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` F ) ` Y ) e. ( Base ` E ) )
28 23 7 6 24 26 27 funcf2 
 |-  ( ph -> ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) : ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) --> ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) H ( ( 1st ` G ) ` ( ( 1st ` F ) ` Y ) ) ) )
29 22 28 feq3dd 
 |-  ( ph -> ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) : ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) --> ( X H Y ) )
30 fcofo 
 |-  ( ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) : ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) --> ( X H Y ) /\ ( X ( 2nd ` F ) Y ) : ( X H Y ) --> ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) /\ ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) = ( _I |` ( X H Y ) ) ) -> ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) : ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) -onto-> ( X H Y ) )
31 29 11 17 30 syl3anc 
 |-  ( ph -> ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) : ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) -onto-> ( X H Y ) )
32 19 31 jca 
 |-  ( ph -> ( ( X ( 2nd ` F ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) /\ ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) : ( ( ( 1st ` F ) ` X ) J ( ( 1st ` F ) ` Y ) ) -onto-> ( X H Y ) ) )