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

Definition df-cat 13886
 Description: A category is an abstraction of a structure (a group, a topology, an order...) Category theory consists in finding new formulation of the concepts associated to those structures (product, substructure...) using morphisms instead of the belonging relation. That trick has the interesting property that heterogeneous structures like topologies or groups for instance become comparable. (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-cat comp
Distinct variable group:   ,,,,,,,,,,

Detailed syntax breakdown of Definition df-cat
StepHypRef Expression
1 ccat 13882 . 2
2 vg . . . . . . . . . . . . . . 15
32cv 1651 . . . . . . . . . . . . . 14
4 vf . . . . . . . . . . . . . . 15
54cv 1651 . . . . . . . . . . . . . 14
6 vy . . . . . . . . . . . . . . . . 17
76cv 1651 . . . . . . . . . . . . . . . 16
8 vx . . . . . . . . . . . . . . . . 17
98cv 1651 . . . . . . . . . . . . . . . 16
107, 9cop 3810 . . . . . . . . . . . . . . 15
11 vo . . . . . . . . . . . . . . . 16
1211cv 1651 . . . . . . . . . . . . . . 15
1310, 9, 12co 6074 . . . . . . . . . . . . . 14
143, 5, 13co 6074 . . . . . . . . . . . . 13
1514, 5wceq 1652 . . . . . . . . . . . 12
16 vh . . . . . . . . . . . . . 14
1716cv 1651 . . . . . . . . . . . . 13
187, 9, 17co 6074 . . . . . . . . . . . 12
1915, 4, 18wral 2698 . . . . . . . . . . 11
209, 9cop 3810 . . . . . . . . . . . . . . 15
2120, 7, 12co 6074 . . . . . . . . . . . . . 14
225, 3, 21co 6074 . . . . . . . . . . . . 13
2322, 5wceq 1652 . . . . . . . . . . . 12
249, 7, 17co 6074 . . . . . . . . . . . 12
2523, 4, 24wral 2698 . . . . . . . . . . 11
2619, 25wa 359 . . . . . . . . . 10
27 vb . . . . . . . . . . 11
2827cv 1651 . . . . . . . . . 10
2926, 6, 28wral 2698 . . . . . . . . 9
309, 9, 17co 6074 . . . . . . . . 9
3129, 2, 30wrex 2699 . . . . . . . 8
329, 7cop 3810 . . . . . . . . . . . . . . . 16
33 vz . . . . . . . . . . . . . . . . 17
3433cv 1651 . . . . . . . . . . . . . . . 16
3532, 34, 12co 6074 . . . . . . . . . . . . . . 15
363, 5, 35co 6074 . . . . . . . . . . . . . 14
379, 34, 17co 6074 . . . . . . . . . . . . . 14
3836, 37wcel 1725 . . . . . . . . . . . . 13
39 vk . . . . . . . . . . . . . . . . . . 19
4039cv 1651 . . . . . . . . . . . . . . . . . 18
417, 34cop 3810 . . . . . . . . . . . . . . . . . . 19
42 vw . . . . . . . . . . . . . . . . . . . 20
4342cv 1651 . . . . . . . . . . . . . . . . . . 19
4441, 43, 12co 6074 . . . . . . . . . . . . . . . . . 18
4540, 3, 44co 6074 . . . . . . . . . . . . . . . . 17
4632, 43, 12co 6074 . . . . . . . . . . . . . . . . 17
4745, 5, 46co 6074 . . . . . . . . . . . . . . . 16
489, 34cop 3810 . . . . . . . . . . . . . . . . . 18
4948, 43, 12co 6074 . . . . . . . . . . . . . . . . 17
5040, 36, 49co 6074 . . . . . . . . . . . . . . . 16
5147, 50wceq 1652 . . . . . . . . . . . . . . 15
5234, 43, 17co 6074 . . . . . . . . . . . . . . 15
5351, 39, 52wral 2698 . . . . . . . . . . . . . 14
5453, 42, 28wral 2698 . . . . . . . . . . . . 13
5538, 54wa 359 . . . . . . . . . . . 12
567, 34, 17co 6074 . . . . . . . . . . . 12
5755, 2, 56wral 2698 . . . . . . . . . . 11
5857, 4, 24wral 2698 . . . . . . . . . 10
5958, 33, 28wral 2698 . . . . . . . . 9
6059, 6, 28wral 2698 . . . . . . . 8
6131, 60wa 359 . . . . . . 7
6261, 8, 28wral 2698 . . . . . 6
63 vc . . . . . . . 8
6463cv 1651 . . . . . . 7
65 cco 13534 . . . . . . 7 comp
6664, 65cfv 5447 . . . . . 6 comp
6762, 11, 66wsbc 3154 . . . . 5 comp
68 chom 13533 . . . . . 6
6964, 68cfv 5447 . . . . 5
7067, 16, 69wsbc 3154 . . . 4 comp
71 cbs 13462 . . . . 5
7264, 71cfv 5447 . . . 4
7370, 27, 72wsbc 3154 . . 3 comp
7473, 63cab 2422 . 2 comp
751, 74wceq 1652 1 comp
 Colors of variables: wff set class This definition is referenced by:  iscat  13890
 Copyright terms: Public domain W3C validator