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

Definition df-cat 16250
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 with 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. Definition in [Lang] p. 53. In contrast to definition 3.1 of [Adamek] p. 21, where "A category is a quadruple A = (O, hom, id, o)", a category is defined as an extensible structure consisting of three slots: the objects "O" ((Base‘𝑐)), the morphisms "hom" ((Hom ‘𝑐)) and the composition law "o" ((comp‘𝑐)). The identities "id" are defined by their properties related to morphisms and their composition, see condition 3.1(b) in [Adamek] p. 21 and df-cid 16251. (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 Cat = {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
Distinct variable group:   𝑏,𝑐,𝑓,𝑔,,𝑘,𝑜,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-cat
StepHypRef Expression
1 ccat 16246 . 2 class Cat
2 vg . . . . . . . . . . . . . . 15 setvar 𝑔
32cv 1479 . . . . . . . . . . . . . 14 class 𝑔
4 vf . . . . . . . . . . . . . . 15 setvar 𝑓
54cv 1479 . . . . . . . . . . . . . 14 class 𝑓
6 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
76cv 1479 . . . . . . . . . . . . . . . 16 class 𝑦
8 vx . . . . . . . . . . . . . . . . 17 setvar 𝑥
98cv 1479 . . . . . . . . . . . . . . . 16 class 𝑥
107, 9cop 4154 . . . . . . . . . . . . . . 15 class 𝑦, 𝑥
11 vo . . . . . . . . . . . . . . . 16 setvar 𝑜
1211cv 1479 . . . . . . . . . . . . . . 15 class 𝑜
1310, 9, 12co 6604 . . . . . . . . . . . . . 14 class (⟨𝑦, 𝑥𝑜𝑥)
143, 5, 13co 6604 . . . . . . . . . . . . 13 class (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓)
1514, 5wceq 1480 . . . . . . . . . . . 12 wff (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
16 vh . . . . . . . . . . . . . 14 setvar
1716cv 1479 . . . . . . . . . . . . 13 class
187, 9, 17co 6604 . . . . . . . . . . . 12 class (𝑦𝑥)
1915, 4, 18wral 2907 . . . . . . . . . . 11 wff 𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
209, 9cop 4154 . . . . . . . . . . . . . . 15 class 𝑥, 𝑥
2120, 7, 12co 6604 . . . . . . . . . . . . . 14 class (⟨𝑥, 𝑥𝑜𝑦)
225, 3, 21co 6604 . . . . . . . . . . . . 13 class (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔)
2322, 5wceq 1480 . . . . . . . . . . . 12 wff (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
249, 7, 17co 6604 . . . . . . . . . . . 12 class (𝑥𝑦)
2523, 4, 24wral 2907 . . . . . . . . . . 11 wff 𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
2619, 25wa 384 . . . . . . . . . 10 wff (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
27 vb . . . . . . . . . . 11 setvar 𝑏
2827cv 1479 . . . . . . . . . 10 class 𝑏
2926, 6, 28wral 2907 . . . . . . . . 9 wff 𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
309, 9, 17co 6604 . . . . . . . . 9 class (𝑥𝑥)
3129, 2, 30wrex 2908 . . . . . . . 8 wff 𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
329, 7cop 4154 . . . . . . . . . . . . . . . 16 class 𝑥, 𝑦
33 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
3433cv 1479 . . . . . . . . . . . . . . . 16 class 𝑧
3532, 34, 12co 6604 . . . . . . . . . . . . . . 15 class (⟨𝑥, 𝑦𝑜𝑧)
363, 5, 35co 6604 . . . . . . . . . . . . . 14 class (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)
379, 34, 17co 6604 . . . . . . . . . . . . . 14 class (𝑥𝑧)
3836, 37wcel 1987 . . . . . . . . . . . . 13 wff (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧)
39 vk . . . . . . . . . . . . . . . . . . 19 setvar 𝑘
4039cv 1479 . . . . . . . . . . . . . . . . . 18 class 𝑘
417, 34cop 4154 . . . . . . . . . . . . . . . . . . 19 class 𝑦, 𝑧
42 vw . . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
4342cv 1479 . . . . . . . . . . . . . . . . . . 19 class 𝑤
4441, 43, 12co 6604 . . . . . . . . . . . . . . . . . 18 class (⟨𝑦, 𝑧𝑜𝑤)
4540, 3, 44co 6604 . . . . . . . . . . . . . . . . 17 class (𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)
4632, 43, 12co 6604 . . . . . . . . . . . . . . . . 17 class (⟨𝑥, 𝑦𝑜𝑤)
4745, 5, 46co 6604 . . . . . . . . . . . . . . . 16 class ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓)
489, 34cop 4154 . . . . . . . . . . . . . . . . . 18 class 𝑥, 𝑧
4948, 43, 12co 6604 . . . . . . . . . . . . . . . . 17 class (⟨𝑥, 𝑧𝑜𝑤)
5040, 36, 49co 6604 . . . . . . . . . . . . . . . 16 class (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5147, 50wceq 1480 . . . . . . . . . . . . . . 15 wff ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5234, 43, 17co 6604 . . . . . . . . . . . . . . 15 class (𝑧𝑤)
5351, 39, 52wral 2907 . . . . . . . . . . . . . 14 wff 𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5453, 42, 28wral 2907 . . . . . . . . . . . . 13 wff 𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5538, 54wa 384 . . . . . . . . . . . 12 wff ((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
567, 34, 17co 6604 . . . . . . . . . . . 12 class (𝑦𝑧)
5755, 2, 56wral 2907 . . . . . . . . . . 11 wff 𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
5857, 4, 24wral 2907 . . . . . . . . . 10 wff 𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
5958, 33, 28wral 2907 . . . . . . . . 9 wff 𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
6059, 6, 28wral 2907 . . . . . . . 8 wff 𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
6131, 60wa 384 . . . . . . 7 wff (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
6261, 8, 28wral 2907 . . . . . 6 wff 𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
63 vc . . . . . . . 8 setvar 𝑐
6463cv 1479 . . . . . . 7 class 𝑐
65 cco 15874 . . . . . . 7 class comp
6664, 65cfv 5847 . . . . . 6 class (comp‘𝑐)
6762, 11, 66wsbc 3417 . . . . 5 wff [(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
68 chom 15873 . . . . . 6 class Hom
6964, 68cfv 5847 . . . . 5 class (Hom ‘𝑐)
7067, 16, 69wsbc 3417 . . . 4 wff [(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
71 cbs 15781 . . . . 5 class Base
7264, 71cfv 5847 . . . 4 class (Base‘𝑐)
7370, 27, 72wsbc 3417 . . 3 wff [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
7473, 63cab 2607 . 2 class {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
751, 74wceq 1480 1 wff Cat = {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
Colors of variables: wff setvar class
This definition is referenced by:  iscat  16254
  Copyright terms: Public domain W3C validator