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