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

Metamath Proof Explorer

Theorem cofidf1a

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

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