cofidf2

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	cofidval.i	$⊢ I = {id}_{func} (D)$
	cofidval.b	$⊢ B = {Base}_{D}$
	cofidval.f	$⊢ φ \to F (D Func E) G$
	cofidval.k	$⊢ φ \to K (E Func D) L$
	cofidval.o	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨F, G⟩ = I$
	cofidval.h	$⊢ H = Hom (D)$
	cofidf2.j	$⊢ J = Hom (E)$
	cofidf2.x	$⊢ φ \to X \in B$
	cofidf2.y	$⊢ φ \to Y \in B$
Assertion	cofidf2	$⊢ φ \to ((X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y) \land (F (X) L F (Y)) : F (X) J F (Y) \underset{onto}{⟶} X H Y)$

Proof

Step	Hyp	Ref	Expression
1		cofidval.i	$⊢ I = {id}_{func} (D)$
2		cofidval.b	$⊢ B = {Base}_{D}$
3		cofidval.f	$⊢ φ \to F (D Func E) G$
4		cofidval.k	$⊢ φ \to K (E Func D) L$
5		cofidval.o	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨F, G⟩ = I$
6		cofidval.h	$⊢ H = Hom (D)$
7		cofidf2.j	$⊢ J = Hom (E)$
8		cofidf2.x	$⊢ φ \to X \in B$
9		cofidf2.y	$⊢ φ \to Y \in B$
10		df-br	$⊢ F (D Func E) G \leftrightarrow ⟨F, G⟩ \in (D Func E)$
11	3 10	sylib	$⊢ φ \to ⟨F, G⟩ \in (D Func E)$
12		df-br	$⊢ K (E Func D) L \leftrightarrow ⟨K, L⟩ \in (E Func D)$
13	4 12	sylib	$⊢ φ \to ⟨K, L⟩ \in (E Func D)$
14	1 2 11 13 5 6 7 8 9	cofidf2a	$⊢ φ \to ((X 2^{nd} (⟨F, G⟩) Y) : X H Y \underset{1-1}{⟶} 1^{st} (⟨F, G⟩) (X) J 1^{st} (⟨F, G⟩) (Y) \land (1^{st} (⟨F, G⟩) (X) 2^{nd} (⟨K, L⟩) 1^{st} (⟨F, G⟩) (Y)) : 1^{st} (⟨F, G⟩) (X) J 1^{st} (⟨F, G⟩) (Y) \underset{onto}{⟶} X H Y)$
15	3	func2nd	$⊢ φ \to 2^{nd} (⟨F, G⟩) = G$
16	15	oveqd	$⊢ φ \to X 2^{nd} (⟨F, G⟩) Y = X G Y$
17		eqidd	$⊢ φ \to X H Y = X H Y$
18	3	func1st	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
19	18	fveq1d	$⊢ φ \to 1^{st} (⟨F, G⟩) (X) = F (X)$
20	18	fveq1d	$⊢ φ \to 1^{st} (⟨F, G⟩) (Y) = F (Y)$
21	19 20	oveq12d	$⊢ φ \to 1^{st} (⟨F, G⟩) (X) J 1^{st} (⟨F, G⟩) (Y) = F (X) J F (Y)$
22	16 17 21	f1eq123d	$⊢ φ \to ((X 2^{nd} (⟨F, G⟩) Y) : X H Y \underset{1-1}{⟶} 1^{st} (⟨F, G⟩) (X) J 1^{st} (⟨F, G⟩) (Y) \leftrightarrow (X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y))$
23	4	func2nd	$⊢ φ \to 2^{nd} (⟨K, L⟩) = L$
24	23 19 20	oveq123d	$⊢ φ \to 1^{st} (⟨F, G⟩) (X) 2^{nd} (⟨K, L⟩) 1^{st} (⟨F, G⟩) (Y) = F (X) L F (Y)$
25	24 21 17	foeq123d	$⊢ φ \to ((1^{st} (⟨F, G⟩) (X) 2^{nd} (⟨K, L⟩) 1^{st} (⟨F, G⟩) (Y)) : 1^{st} (⟨F, G⟩) (X) J 1^{st} (⟨F, G⟩) (Y) \underset{onto}{⟶} X H Y \leftrightarrow (F (X) L F (Y)) : F (X) J F (Y) \underset{onto}{⟶} X H Y)$
26	22 25	anbi12d	$⊢ φ \to (((X 2^{nd} (⟨F, G⟩) Y) : X H Y \underset{1-1}{⟶} 1^{st} (⟨F, G⟩) (X) J 1^{st} (⟨F, G⟩) (Y) \land (1^{st} (⟨F, G⟩) (X) 2^{nd} (⟨K, L⟩) 1^{st} (⟨F, G⟩) (Y)) : 1^{st} (⟨F, G⟩) (X) J 1^{st} (⟨F, G⟩) (Y) \underset{onto}{⟶} X H Y) \leftrightarrow ((X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y) \land (F (X) L F (Y)) : F (X) J F (Y) \underset{onto}{⟶} X H Y))$
27	14 26	mpbid	$⊢ φ \to ((X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y) \land (F (X) L F (Y)) : F (X) J F (Y) \underset{onto}{⟶} X H Y)$

Metamath Proof Explorer

Theorem cofidf2

Proof