Metamath Proof Explorer

Theorem cofidf2

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 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 )
cofidf2.j 
|- J = ( Hom ` E )
cofidf2.x 
|- ( ph -> X e. B )
cofidf2.y 
|- ( ph -> Y e. B )
Assertion cofidf2 
|- ( ph -> ( ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) /\ ( ( F ` X ) L ( F ` Y ) ) : ( ( F ` X ) J ( F ` Y ) ) -onto-> ( X H Y ) ) )

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 cofidf2.j 
 |-  J = ( Hom ` E )
8 cofidf2.x 
 |-  ( ph -> X e. B )
9 cofidf2.y 
 |-  ( ph -> Y e. B )
10 df-br 
 |-  ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) )
11 3 10 sylib 
 |-  ( ph -> <. F , G >. e. ( D Func E ) )
12 df-br 
 |-  ( K ( E Func D ) L <-> <. K , L >. e. ( E Func D ) )
13 4 12 sylib 
 |-  ( ph -> <. K , L >. e. ( E Func D ) )
14 1 2 11 13 5 6 7 8 9 cofidf2a 
 |-  ( ph -> ( ( X ( 2nd ` <. F , G >. ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` <. F , G >. ) ` X ) J ( ( 1st ` <. F , G >. ) ` Y ) ) /\ ( ( ( 1st ` <. F , G >. ) ` X ) ( 2nd ` <. K , L >. ) ( ( 1st ` <. F , G >. ) ` Y ) ) : ( ( ( 1st ` <. F , G >. ) ` X ) J ( ( 1st ` <. F , G >. ) ` Y ) ) -onto-> ( X H Y ) ) )
15 3 func2nd 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )
16 15 oveqd 
 |-  ( ph -> ( X ( 2nd ` <. F , G >. ) Y ) = ( X G Y ) )
17 eqidd 
 |-  ( ph -> ( X H Y ) = ( X H Y ) )
18 3 func1st 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
19 18 fveq1d 
 |-  ( ph -> ( ( 1st ` <. F , G >. ) ` X ) = ( F ` X ) )
20 18 fveq1d 
 |-  ( ph -> ( ( 1st ` <. F , G >. ) ` Y ) = ( F ` Y ) )
21 19 20 oveq12d 
 |-  ( ph -> ( ( ( 1st ` <. F , G >. ) ` X ) J ( ( 1st ` <. F , G >. ) ` Y ) ) = ( ( F ` X ) J ( F ` Y ) ) )
22 16 17 21 f1eq123d 
 |-  ( ph -> ( ( X ( 2nd ` <. F , G >. ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` <. F , G >. ) ` X ) J ( ( 1st ` <. F , G >. ) ` Y ) ) <-> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) ) )
23 4 func2nd 
 |-  ( ph -> ( 2nd ` <. K , L >. ) = L )
24 23 19 20 oveq123d 
 |-  ( ph -> ( ( ( 1st ` <. F , G >. ) ` X ) ( 2nd ` <. K , L >. ) ( ( 1st ` <. F , G >. ) ` Y ) ) = ( ( F ` X ) L ( F ` Y ) ) )
25 24 21 17 foeq123d 
 |-  ( ph -> ( ( ( ( 1st ` <. F , G >. ) ` X ) ( 2nd ` <. K , L >. ) ( ( 1st ` <. F , G >. ) ` Y ) ) : ( ( ( 1st ` <. F , G >. ) ` X ) J ( ( 1st ` <. F , G >. ) ` Y ) ) -onto-> ( X H Y ) <-> ( ( F ` X ) L ( F ` Y ) ) : ( ( F ` X ) J ( F ` Y ) ) -onto-> ( X H Y ) ) )
26 22 25 anbi12d 
 |-  ( ph -> ( ( ( X ( 2nd ` <. F , G >. ) Y ) : ( X H Y ) -1-1-> ( ( ( 1st ` <. F , G >. ) ` X ) J ( ( 1st ` <. F , G >. ) ` Y ) ) /\ ( ( ( 1st ` <. F , G >. ) ` X ) ( 2nd ` <. K , L >. ) ( ( 1st ` <. F , G >. ) ` Y ) ) : ( ( ( 1st ` <. F , G >. ) ` X ) J ( ( 1st ` <. F , G >. ) ` Y ) ) -onto-> ( X H Y ) ) <-> ( ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) /\ ( ( F ` X ) L ( F ` Y ) ) : ( ( F ` X ) J ( F ` Y ) ) -onto-> ( X H Y ) ) ) )
27 14 26 mpbid 
 |-  ( ph -> ( ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) /\ ( ( F ` X ) L ( F ` Y ) ) : ( ( F ` X ) J ( F ` Y ) ) -onto-> ( X H Y ) ) )