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={id}_{\mathrm{func}}\left(D\right)$$
	cofidvala.b	$$⊢B={\mathrm{Base}}_D$$
	cofidvala.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
	cofidvala.g	$$⊢\phi \to G\in \left(E\mathrm{Func}D\right)$$
	cofidvala.o	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=I$$
	cofidf1a.c	$$⊢C={\mathrm{Base}}_E$$
Assertion	cofidf1a	$$⊢\phi \to \left(1^{st}\left(F\right):B\underset{1-1}{⟶}C\wedge 1^{st}\left(G\right):C\underset{onto}{⟶}B\right)$$

Proof

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