Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rocatset Unicode version

Definition df-rocatset 26059
 Description: Composition of two morphisms in the category Set. Experimental. (Contributed by FL, 6-Nov-2013.)
Assertion
Ref Expression
df-rocatset
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-rocatset
StepHypRef Expression
1 crocase 26058 . 2
2 vx . . 3
3 cgru 8428 . . 3
4 va . . . . . . . 8
54cv 1631 . . . . . . 7
62cv 1631 . . . . . . . 8
7 ccmrcase 26013 . . . . . . . 8
86, 7cfv 5271 . . . . . . 7
95, 8wcel 1696 . . . . . 6
10 vb . . . . . . . 8
1110cv 1631 . . . . . . 7
1211, 8wcel 1696 . . . . . 6
13 c1st 6136 . . . . . . . . 9
1413, 13ccom 4709 . . . . . . . 8
155, 14cfv 5271 . . . . . . 7
16 c2nd 6137 . . . . . . . . 9
1716, 13ccom 4709 . . . . . . . 8
1811, 17cfv 5271 . . . . . . 7
1915, 18wceq 1632 . . . . . 6
209, 12, 19w3a 934 . . . . 5
21 vc . . . . . . 7
2221cv 1631 . . . . . 6
2311, 14cfv 5271 . . . . . . . 8
245, 17cfv 5271 . . . . . . . 8
2523, 24cop 3656 . . . . . . 7
265, 16cfv 5271 . . . . . . . 8
2711, 16cfv 5271 . . . . . . . 8
2826, 27ccom 4709 . . . . . . 7
2925, 28cop 3656 . . . . . 6
3022, 29wceq 1632 . . . . 5
3120, 30wa 358 . . . 4
3231, 4, 10, 21coprab 5875 . . 3
332, 3, 32cmpt 4093 . 2
341, 33wceq 1632 1
 Colors of variables: wff set class This definition is referenced by:  isrocatset  26060
 Copyright terms: Public domain W3C validator