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 ) )