This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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}_{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$
		cofidf1.c	$⊢ C = {Base}_{E}$
	Assertion	cofidf1	$⊢ φ \to (F : B \underset{1-1}{⟶} C \land K : C \underset{onto}{⟶} B)$

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		cofidf1.c	$⊢ C = {Base}_{E}$
7	2 6 3	funcf1	$⊢ φ \to F : B ⟶ C$
8		eqid	$⊢ Hom (D) = Hom (D)$
9	1 2 3 4 5 8	cofidval	$⊢ φ \to (K \circ F = {I ↾}_{B} \land (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y)) = (z \in (B \times B) ⟼ {I ↾}_{Hom (D) (z)}))$
10	9	simpld	$⊢ φ \to K \circ F = {I ↾}_{B}$
11		fcof1	$⊢ (F : B ⟶ C \land K \circ F = {I ↾}_{B}) \to F : B \underset{1-1}{⟶} C$
12	7 10 11	syl2anc	$⊢ φ \to F : B \underset{1-1}{⟶} C$
13	6 2 4	funcf1	$⊢ φ \to K : C ⟶ B$
14		fcofo	$⊢ (K : C ⟶ B \land F : B ⟶ C \land K \circ F = {I ↾}_{B}) \to K : C \underset{onto}{⟶} B$
15	13 7 10 14	syl3anc	$⊢ φ \to K : C \underset{onto}{⟶} B$
16	12 15	jca	$⊢ φ \to (F : B \underset{1-1}{⟶} C \land K : C \underset{onto}{⟶} B)$