Definition df-sect 15652

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

Assertion

Ref	Expression
df-sect	|- Sect = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. (comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )

Distinct variable group:   f, c, g, h, x, y

Detailed syntax breakdown of Definition df-sect

Step	Hyp	Ref	Expression
1		csect 15649	. 2 class Sect
2		vc	. . 3 setvar c
3		ccat 15570	. . 3 class Cat
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1443	. . . . 5 class c
7		cbs 15121	. . . . 5 class Base
8	6, 7	cfv 5582	. . . 4 class ( Base ` c )
9		vf	. . . . . . . . . 10 setvar f
10	9	cv 1443	. . . . . . . . 9 class f
11	4	cv 1443	. . . . . . . . . 10 class x
12	5	cv 1443	. . . . . . . . . 10 class y
13		vh	. . . . . . . . . . 11 setvar h
14	13	cv 1443	. . . . . . . . . 10 class h
15	11, 12, 14	co 6290	. . . . . . . . 9 class ( x h y )
16	10, 15	wcel 1887	. . . . . . . 8 wff f e. ( x h y )
17		vg	. . . . . . . . . 10 setvar g
18	17	cv 1443	. . . . . . . . 9 class g
19	12, 11, 14	co 6290	. . . . . . . . 9 class ( y h x )
20	18, 19	wcel 1887	. . . . . . . 8 wff g e. ( y h x )
21	16, 20	wa 371	. . . . . . 7 wff ( f e. ( x h y ) /\ g e. ( y h x ) )
22	11, 12	cop 3974	. . . . . . . . . 10 class <. x , y >.
23		cco 15202	. . . . . . . . . . 11 class comp
24	6, 23	cfv 5582	. . . . . . . . . 10 class (comp ` c )
25	22, 11, 24	co 6290	. . . . . . . . 9 class ( <. x , y >. (comp ` c ) x )
26	18, 10, 25	co 6290	. . . . . . . 8 class ( g ( <. x , y >. (comp ` c ) x ) f )
27		ccid 15571	. . . . . . . . . 10 class Id
28	6, 27	cfv 5582	. . . . . . . . 9 class ( Id ` c )
29	11, 28	cfv 5582	. . . . . . . 8 class ( ( Id ` c ) ` x )
30	26, 29	wceq 1444	. . . . . . 7 wff ( g ( <. x , y >. (comp ` c ) x ) f ) = ( ( Id ` c ) ` x )
31	21, 30	wa 371	. . . . . 6 wff ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. (comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) )
32		chom 15201	. . . . . . 7 class Hom
33	6, 32	cfv 5582	. . . . . 6 class ( Hom ` c )
34	31, 13, 33	wsbc 3267	. . . . 5 wff [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. (comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) )
35	34, 9, 17	copab 4460	. . . 4 class { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. (comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) }
36	4, 5, 8, 8, 35	cmpt2 6292	. . 3 class ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. (comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } )
37	2, 3, 36	cmpt 4461	. 2 class ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. (comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )
38	1, 37	wceq 1444	1 wff Sect = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. (comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )

This definition is referenced by:  sectffval  15655