catcsect

Description: The property " F is a section of G " in a category of small categories (in a universe). (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	catcsect.c	$⊢ C = CatCat (U)$
	catcsect.h	$⊢ H = Hom (C)$
	catcsect.i	$⊢ I = {id}_{func} (X)$
	catcsect.s	$⊢ S = Sect (C)$
Assertion	catcsect	$⊢ F (X S Y) G \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land G \circ_{func} F = I)$

Proof

Step	Hyp	Ref	Expression
1		catcsect.c	$⊢ C = CatCat (U)$
2		catcsect.h	$⊢ H = Hom (C)$
3		catcsect.i	$⊢ I = {id}_{func} (X)$
4		catcsect.s	$⊢ S = Sect (C)$
5		id	$⊢ F (X S Y) G \to F (X S Y) G$
6	4 5	sectrcl	$⊢ F (X S Y) G \to C \in Cat$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8	4 5 7	sectrcl2	$⊢ F (X S Y) G \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
9	6 8	jca	$⊢ F (X S Y) G \to (C \in Cat \land (X \in {Base}_{C} \land Y \in {Base}_{C}))$
10		simpl	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to F \in (X H Y)$
11	1 2 10	catcrcl	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to U \in V$
12	1	catccat	$⊢ U \in V \to C \in Cat$
13	11 12	syl	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to C \in Cat$
14	1 2 10 7	catcrcl2	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
15	13 14	jca	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to (C \in Cat \land (X \in {Base}_{C} \land Y \in {Base}_{C}))$
16	15	3adant3	$⊢ (F \in (X H Y) \land G \in (Y H X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \to (C \in Cat \land (X \in {Base}_{C} \land Y \in {Base}_{C}))$
17		eqid	$⊢ comp (C) = comp (C)$
18		eqid	$⊢ Id (C) = Id (C)$
19		simpl	$⊢ (C \in Cat \land (X \in {Base}_{C} \land Y \in {Base}_{C})) \to C \in Cat$
20		simprl	$⊢ (C \in Cat \land (X \in {Base}_{C} \land Y \in {Base}_{C})) \to X \in {Base}_{C}$
21		simprr	$⊢ (C \in Cat \land (X \in {Base}_{C} \land Y \in {Base}_{C})) \to Y \in {Base}_{C}$
22	7 2 17 18 4 19 20 21	issect	$⊢ (C \in Cat \land (X \in {Base}_{C} \land Y \in {Base}_{C})) \to (F (X S Y) G \leftrightarrow (F \in (X H Y) \land G \in (Y H X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
23	9 16 22	pm5.21nii	$⊢ F (X S Y) G \leftrightarrow (F \in (X H Y) \land G \in (Y H X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X))$
24		df-3an	$⊢ (F \in (X H Y) \land G \in (Y H X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X))$
25	15 20	syl	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to X \in {Base}_{C}$
26	15 21	syl	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to Y \in {Base}_{C}$
27	1 2 10	elcatchom	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to F \in (X Func Y)$
28		simpr	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to G \in (Y H X)$
29	1 2 28	elcatchom	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to G \in (Y Func X)$
30	1 7 11 17 25 26 25 27 29	catcco	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to G (⟨X, Y⟩ comp (C) X) F = G \circ_{func} F$
31	1 7 18 3 11 25	catcid	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to Id (C) (X) = I$
32	30 31	eqeq12d	$⊢ (F \in (X H Y) \land G \in (Y H X)) \to (G (⟨X, Y⟩ comp (C) X) F = Id (C) (X) \leftrightarrow G \circ_{func} F = I)$
33	32	pm5.32i	$⊢ ((F \in (X H Y) \land G \in (Y H X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land G \circ_{func} F = I)$
34	23 24 33	3bitri	$⊢ F (X S Y) G \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land G \circ_{func} F = I)$

Metamath Proof Explorer

Theorem catcsect

Proof