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

Definition df-sect 13975
 Description: Function returning the section relation in a category. Given arrows and , we say Sect, that is, is a section of , if . (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 13972 . 2 Sect
2 vc . . 3
3 ccat 13891 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1652 . . . . 5
7 cbs 13471 . . . . 5
86, 7cfv 5456 . . . 4
9 vf . . . . . . . . . 10
109cv 1652 . . . . . . . . 9
114cv 1652 . . . . . . . . . 10
125cv 1652 . . . . . . . . . 10
13 vh . . . . . . . . . . 11
1413cv 1652 . . . . . . . . . 10
1511, 12, 14co 6083 . . . . . . . . 9
1610, 15wcel 1726 . . . . . . . 8
17 vg . . . . . . . . . 10
1817cv 1652 . . . . . . . . 9
1912, 11, 14co 6083 . . . . . . . . 9
2018, 19wcel 1726 . . . . . . . 8
2116, 20wa 360 . . . . . . 7
2211, 12cop 3819 . . . . . . . . . 10
23 cco 13543 . . . . . . . . . . 11 comp
246, 23cfv 5456 . . . . . . . . . 10 comp
2522, 11, 24co 6083 . . . . . . . . 9 comp
2618, 10, 25co 6083 . . . . . . . 8 comp
27 ccid 13892 . . . . . . . . . 10
286, 27cfv 5456 . . . . . . . . 9
2911, 28cfv 5456 . . . . . . . 8
3026, 29wceq 1653 . . . . . . 7 comp
3121, 30wa 360 . . . . . 6 comp
32 chom 13542 . . . . . . 7
336, 32cfv 5456 . . . . . 6
3431, 13, 33wsbc 3163 . . . . 5 comp
3534, 9, 17copab 4267 . . . 4 comp
364, 5, 8, 8, 35cmpt2 6085 . . 3 comp
372, 3, 36cmpt 4268 . 2 comp
381, 37wceq 1653 1 Sect comp
 Colors of variables: wff set class This definition is referenced by:  sectffval  13978
 Copyright terms: Public domain W3C validator