df-sect

Description: Function returning the section relation in a category. Given arrows f : X --> Y and g : Y --> X , we say f Sect g , that is, f is a section of g , if g o. f = 1X . If there there is an arrow g with f Sect g , the arrow f is called a section, see definition 7.19 of Adamek p. 106. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Assertion	df-sect	$⊢ Sect = (c \in Cat ⟼ (x \in {Base}_{c}, y \in {Base}_{c} ⟼ \{⟨f, g⟩ \| \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csect	$class Sect$
1		vc	$setvar c$
2		ccat	$class Cat$
3		vx	$setvar x$
4		cbs	$class Base$
5	1	cv	$setvar c$
6	5 4	cfv	$class {Base}_{c}$
7		vy	$setvar y$
8		vf	$setvar f$
9		vg	$setvar g$
10		chom	$class Hom$
11	5 10	cfv	$class Hom (c)$
12		vh	$setvar h$
13	8	cv	$setvar f$
14	3	cv	$setvar x$
15	12	cv	$setvar h$
16	7	cv	$setvar y$
17	14 16 15	co	$class (x h y)$
18	13 17	wcel	$wff f \in (x h y)$
19	9	cv	$setvar g$
20	16 14 15	co	$class (y h x)$
21	19 20	wcel	$wff g \in (y h x)$
22	18 21	wa	$wff (f \in (x h y) \land g \in (y h x))$
23	14 16	cop	$class ⟨x, y⟩$
24		cco	$class comp$
25	5 24	cfv	$class comp (c)$
26	23 14 25	co	$class (⟨x, y⟩ comp (c) x)$
27	19 13 26	co	$class (g (⟨x, y⟩ comp (c) x) f)$
28		ccid	$class Id$
29	5 28	cfv	$class Id (c)$
30	14 29	cfv	$class Id (c) (x)$
31	27 30	wceq	$wff g (⟨x, y⟩ comp (c) x) f = Id (c) (x)$
32	22 31	wa	$wff ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))$
33	32 12 11	wsbc	$wff \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))$
34	33 8 9	copab	$class \{⟨f, g⟩ \| \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))\}$
35	3 7 6 6 34	cmpo	$class (x \in {Base}_{c}, y \in {Base}_{c} ⟼ \{⟨f, g⟩ \| \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))\})$
36	1 2 35	cmpt	$class (c \in Cat ⟼ (x \in {Base}_{c}, y \in {Base}_{c} ⟼ \{⟨f, g⟩ \| \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))\}))$
37	0 36	wceq	$wff Sect = (c \in Cat ⟼ (x \in {Base}_{c}, y \in {Base}_{c} ⟼ \{⟨f, g⟩ \| \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))\}))$

Metamath Proof Explorer

Definition df-sect

Detailed syntax breakdown