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={id}_{\mathrm{func}}\left(D\right)$$
	cofidval.b	$$⊢B={\mathrm{Base}}_D$$
	cofidval.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
	cofidval.k	$$⊢\phi \to K\left(E\mathrm{Func}D\right)L$$
	cofidval.o	$$⊢\phi \to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩=I$$
	cofidf1.c	$$⊢C={\mathrm{Base}}_E$$
Assertion	cofidf1	$$⊢\phi \to \left(F:B\underset{1-1}{⟶}C\wedge K:C\underset{onto}{⟶}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		cofidval.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
2		cofidval.b	$$⊢B={\mathrm{Base}}_D$$
3		cofidval.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
4		cofidval.k	$$⊢\phi \to K\left(E\mathrm{Func}D\right)L$$
5		cofidval.o	$$⊢\phi \to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩=I$$
6		cofidf1.c	$$⊢C={\mathrm{Base}}_E$$
7	2 6 3	funcf1	$$⊢\phi \to F:B⟶C$$
8		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
9	1 2 3 4 5 8	cofidval	$$⊢\phi \to \left(K\circ F={\mathrm{I}\upharpoonright }_B\wedge \left(x\in B,y\in B⟼\left(F\left(x\right)LF\left(y\right)\right)\circ \left(xGy\right)\right)=\left(z\in \left(B\times B\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(D\right)\left(z\right)}\right)\right)$$
10	9	simpld	$$⊢\phi \to K\circ F={\mathrm{I}\upharpoonright }_B$$
11		fcof1	$$⊢\left(F:B⟶C\wedge K\circ F={\mathrm{I}\upharpoonright }_B\right)\to F:B\underset{1-1}{⟶}C$$
12	7 10 11	syl2anc	$$⊢\phi \to F:B\underset{1-1}{⟶}C$$
13	6 2 4	funcf1	$$⊢\phi \to K:C⟶B$$
14		fcofo	$$⊢\left(K:C⟶B\wedge F:B⟶C\wedge K\circ F={\mathrm{I}\upharpoonright }_B\right)\to K:C\underset{onto}{⟶}B$$
15	13 7 10 14	syl3anc	$$⊢\phi \to K:C\underset{onto}{⟶}B$$
16	12 15	jca	$$⊢\phi \to \left(F:B\underset{1-1}{⟶}C\wedge K:C\underset{onto}{⟶}B\right)$$