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

Metamath Proof Explorer

Theorem cofidf1

Description: If " <. F , G >. is a section of <. K , L >. " in a category of small categories (in a universe), then F is injective, and K is surjective. (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 )
cofidf1.c 
|- C = ( Base ` E )
Assertion cofidf1 
|- ( ph -> ( F : B -1-1-> C /\ K : C -onto-> B ) )

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 cofidf1.c 
 |-  C = ( Base ` E )
7 2 6 3 funcf1 
 |-  ( ph -> F : B --> C )
8 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
9 1 2 3 4 5 8 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 |` ( ( Hom ` D ) ` z ) ) ) ) )
10 9 simpld 
 |-  ( ph -> ( K o. F ) = ( _I |` B ) )
11 fcof1 
 |-  ( ( F : B --> C /\ ( K o. F ) = ( _I |` B ) ) -> F : B -1-1-> C )
12 7 10 11 syl2anc 
 |-  ( ph -> F : B -1-1-> C )
13 6 2 4 funcf1 
 |-  ( ph -> K : C --> B )
14 fcofo 
 |-  ( ( K : C --> B /\ F : B --> C /\ ( K o. F ) = ( _I |` B ) ) -> K : C -onto-> B )
15 13 7 10 14 syl3anc 
 |-  ( ph -> K : C -onto-> B )
16 12 15 jca 
 |-  ( ph -> ( F : B -1-1-> C /\ K : C -onto-> B ) )