Metamath Proof Explorer

Theorem cofidfth

Description: If " F is a section of G " in a category of small categories (in a universe), then F is faithful. Combined with cofidf1 , this theorem proves that F is an embedding (a faithful functor injective on objects, remark 3.28(1) of Adamek p. 34). (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Hypotheses cofidfth.i 
|- I = ( idFunc ` D )
cofidfth.f 
|- ( ph -> F ( D Func E ) G )
cofidfth.k 
|- ( ph -> K ( E Func D ) L )
cofidfth.o 
|- ( ph -> ( <. K , L >. o.func <. F , G >. ) = I )
Assertion cofidfth 
|- ( ph -> F ( D Faith E ) G )

Proof

Step Hyp Ref Expression
1 cofidfth.i 
 |-  I = ( idFunc ` D )
2 cofidfth.f 
 |-  ( ph -> F ( D Func E ) G )
3 cofidfth.k 
 |-  ( ph -> K ( E Func D ) L )
4 cofidfth.o 
 |-  ( ph -> ( <. K , L >. o.func <. F , G >. ) = I )
5 eqid 
 |-  ( Base ` D ) = ( Base ` D )
6 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> F ( D Func E ) G )
7 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> K ( E Func D ) L )
8 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( <. K , L >. o.func <. F , G >. ) = I )
9 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
10 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
11 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> x e. ( Base ` D ) )
12 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
13 1 5 6 7 8 9 10 11 12 cofidf2 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( x G y ) : ( x ( Hom ` D ) y ) -1-1-> ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) /\ ( ( F ` x ) L ( F ` y ) ) : ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) -onto-> ( x ( Hom ` D ) y ) ) )
14 13 simpld 
 |-  ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x G y ) : ( x ( Hom ` D ) y ) -1-1-> ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) )
15 14 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` D ) A. y e. ( Base ` D ) ( x G y ) : ( x ( Hom ` D ) y ) -1-1-> ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) )
16 5 9 10 isfth2 
 |-  ( F ( D Faith E ) G <-> ( F ( D Func E ) G /\ A. x e. ( Base ` D ) A. y e. ( Base ` D ) ( x G y ) : ( x ( Hom ` D ) y ) -1-1-> ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) ) )
17 2 15 16 sylanbrc 
 |-  ( ph -> F ( D Faith E ) G )