Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sect Structured version   Visualization version   Unicode version

Definition df-sect 15652
 Description: Function returning the section relation in a category. Given arrows and , we say Sect, that is, is a section of , if . If there there is an arrow with Sect, the arrow 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 comp
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-sect
StepHypRef Expression
1 csect 15649 . 2 Sect
2 vc . . 3
3 ccat 15570 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1443 . . . . 5
7 cbs 15121 . . . . 5
86, 7cfv 5582 . . . 4
9 vf . . . . . . . . . 10
109cv 1443 . . . . . . . . 9
114cv 1443 . . . . . . . . . 10
125cv 1443 . . . . . . . . . 10
13 vh . . . . . . . . . . 11
1413cv 1443 . . . . . . . . . 10
1511, 12, 14co 6290 . . . . . . . . 9
1610, 15wcel 1887 . . . . . . . 8
17 vg . . . . . . . . . 10
1817cv 1443 . . . . . . . . 9
1912, 11, 14co 6290 . . . . . . . . 9
2018, 19wcel 1887 . . . . . . . 8
2116, 20wa 371 . . . . . . 7
2211, 12cop 3974 . . . . . . . . . 10
23 cco 15202 . . . . . . . . . . 11 comp
246, 23cfv 5582 . . . . . . . . . 10 comp
2522, 11, 24co 6290 . . . . . . . . 9 comp
2618, 10, 25co 6290 . . . . . . . 8 comp
27 ccid 15571 . . . . . . . . . 10
286, 27cfv 5582 . . . . . . . . 9
2911, 28cfv 5582 . . . . . . . 8
3026, 29wceq 1444 . . . . . . 7 comp
3121, 30wa 371 . . . . . 6 comp
32 chom 15201 . . . . . . 7
336, 32cfv 5582 . . . . . 6
3431, 13, 33wsbc 3267 . . . . 5 comp
3534, 9, 17copab 4460 . . . 4 comp
364, 5, 8, 8, 35cmpt2 6292 . . 3 comp
372, 3, 36cmpt 4461 . 2 comp
381, 37wceq 1444 1 Sect comp
 Colors of variables: wff setvar class This definition is referenced by:  sectffval  15655
 Copyright terms: Public domain W3C validator