Theorem cofidf2a

Description: If " F is a section of G " in a category of small categories (in a universe), then the morphism part of F is injective, and the morphism part of G is surjective in the image of F . (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$$
	cofidvala.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	cofidf2a.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
	cofidf2a.x	$$⊢\phi \to X\in B$$
	cofidf2a.y	$$⊢\phi \to Y\in B$$
Assertion	cofidf2a	$$⊢\phi \to \left(\left(X{2}^{nd}\left(F\right)Y\right):XHY\underset{1-1}{⟶}{1}^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)\wedge \left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right):1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)\underset{onto}{⟶}XHY\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		cofidvala.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
7		cofidf2a.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
8		cofidf2a.x	$$⊢\phi \to X\in B$$
9		cofidf2a.y	$$⊢\phi \to Y\in B$$
10	3	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(D\mathrm{Func}E\right)2^{nd}\left(F\right)$$
11	2 6 7 10 8 9	funcf2	$$⊢\phi \to \left(X{2}^{nd}\left(F\right)Y\right):XHY⟶1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)$$
12	5	fveq2d	$$⊢\phi \to 2^{nd}\left(G{\circ }_{\mathrm{func}}F\right)=2^{nd}\left(I\right)$$
13	12	oveqd	$$⊢\phi \to X{2}^{nd}\left(G{\circ }_{\mathrm{func}}F\right)Y=X{2}^{nd}\left(I\right)Y$$
14	2 3 4 8 9	cofu2nd	$$⊢\phi \to X{2}^{nd}\left(G{\circ }_{\mathrm{func}}F\right)Y=\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)$$
15	10	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
16	1 2 15 6 8 9	idfu2nd	$$⊢\phi \to X{2}^{nd}\left(I\right)Y={\mathrm{I}\upharpoonright }_{\left(XHY\right)}$$
17	13 14 16	3eqtr3d	$$⊢\phi \to \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)={\mathrm{I}\upharpoonright }_{\left(XHY\right)}$$
18		fcof1	$$⊢\left(\left(X{2}^{nd}\left(F\right)Y\right):XHY⟶1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)\wedge \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)={\mathrm{I}\upharpoonright }_{\left(XHY\right)}\right)\to \left(X{2}^{nd}\left(F\right)Y\right):XHY\underset{1-1}{⟶}{1}^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)$$
19	11 17 18	syl2anc	$$⊢\phi \to \left(X{2}^{nd}\left(F\right)Y\right):XHY\underset{1-1}{⟶}{1}^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)$$
20	1 2 8 3 4 5	cofid1a	$$⊢\phi \to 1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(X\right)\right)=X$$
21	1 2 9 3 4 5	cofid1a	$$⊢\phi \to 1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(Y\right)\right)=Y$$
22	20 21	oveq12d	$$⊢\phi \to 1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(X\right)\right)H{1}^{st}\left(G\right)\left(1^{st}\left(F\right)\left(Y\right)\right)=XHY$$
23		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
24	4	func1st2nd	$$⊢\phi \to 1^{st}\left(G\right)\left(E\mathrm{Func}D\right)2^{nd}\left(G\right)$$
25	2 23 10	funcf1	$$⊢\phi \to 1^{st}\left(F\right):B⟶{\mathrm{Base}}_E$$
26	25 8	ffvelcdmd	$$⊢\phi \to 1^{st}\left(F\right)\left(X\right)\in {\mathrm{Base}}_E$$
27	25 9	ffvelcdmd	$$⊢\phi \to 1^{st}\left(F\right)\left(Y\right)\in {\mathrm{Base}}_E$$
28	23 7 6 24 26 27	funcf2	$$⊢\phi \to \left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right):1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)⟶1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(X\right)\right)H{1}^{st}\left(G\right)\left(1^{st}\left(F\right)\left(Y\right)\right)$$
29	22 28	feq3dd	$$⊢\phi \to \left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right):1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)⟶XHY$$
30		fcofo	$$⊢\left(\left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right):1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)⟶XHY\wedge \left(X{2}^{nd}\left(F\right)Y\right):XHY⟶1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)\wedge \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)={\mathrm{I}\upharpoonright }_{\left(XHY\right)}\right)\to \left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right):1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)\underset{onto}{⟶}XHY$$
31	29 11 17 30	syl3anc	$$⊢\phi \to \left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right):1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)\underset{onto}{⟶}XHY$$
32	19 31	jca	$$⊢\phi \to \left(\left(X{2}^{nd}\left(F\right)Y\right):XHY\underset{1-1}{⟶}{1}^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)\wedge \left(1^{st}\left(F\right)\left(X\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(Y\right)\right):1^{st}\left(F\right)\left(X\right)J{1}^{st}\left(F\right)\left(Y\right)\underset{onto}{⟶}XHY\right)$$