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 16929
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 16930. (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 16925 . 2 class Cat
2 vg . . . . . . . . . . . . . . 15 setvar 𝑔
32cv 1527 . . . . . . . . . . . . . 14 class 𝑔
4 vf . . . . . . . . . . . . . . 15 setvar 𝑓
54cv 1527 . . . . . . . . . . . . . 14 class 𝑓
6 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
76cv 1527 . . . . . . . . . . . . . . . 16 class 𝑦
8 vx . . . . . . . . . . . . . . . . 17 setvar 𝑥
98cv 1527 . . . . . . . . . . . . . . . 16 class 𝑥
107, 9cop 4565 . . . . . . . . . . . . . . 15 class 𝑦, 𝑥
11 vo . . . . . . . . . . . . . . . 16 setvar 𝑜
1211cv 1527 . . . . . . . . . . . . . . 15 class 𝑜
1310, 9, 12co 7145 . . . . . . . . . . . . . 14 class (⟨𝑦, 𝑥𝑜𝑥)
143, 5, 13co 7145 . . . . . . . . . . . . 13 class (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓)
1514, 5wceq 1528 . . . . . . . . . . . 12 wff (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
16 vh . . . . . . . . . . . . . 14 setvar
1716cv 1527 . . . . . . . . . . . . 13 class
187, 9, 17co 7145 . . . . . . . . . . . 12 class (𝑦𝑥)
1915, 4, 18wral 3138 . . . . . . . . . . 11 wff 𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
209, 9cop 4565 . . . . . . . . . . . . . . 15 class 𝑥, 𝑥
2120, 7, 12co 7145 . . . . . . . . . . . . . 14 class (⟨𝑥, 𝑥𝑜𝑦)
225, 3, 21co 7145 . . . . . . . . . . . . 13 class (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔)
2322, 5wceq 1528 . . . . . . . . . . . 12 wff (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
249, 7, 17co 7145 . . . . . . . . . . . 12 class (𝑥𝑦)
2523, 4, 24wral 3138 . . . . . . . . . . 11 wff 𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
2619, 25wa 396 . . . . . . . . . 10 wff (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
27 vb . . . . . . . . . . 11 setvar 𝑏
2827cv 1527 . . . . . . . . . 10 class 𝑏
2926, 6, 28wral 3138 . . . . . . . . 9 wff 𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
309, 9, 17co 7145 . . . . . . . . 9 class (𝑥𝑥)
3129, 2, 30wrex 3139 . . . . . . . 8 wff 𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
329, 7cop 4565 . . . . . . . . . . . . . . . 16 class 𝑥, 𝑦
33 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
3433cv 1527 . . . . . . . . . . . . . . . 16 class 𝑧
3532, 34, 12co 7145 . . . . . . . . . . . . . . 15 class (⟨𝑥, 𝑦𝑜𝑧)
363, 5, 35co 7145 . . . . . . . . . . . . . 14 class (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)
379, 34, 17co 7145 . . . . . . . . . . . . . 14 class (𝑥𝑧)
3836, 37wcel 2105 . . . . . . . . . . . . 13 wff (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧)
39 vk . . . . . . . . . . . . . . . . . . 19 setvar 𝑘
4039cv 1527 . . . . . . . . . . . . . . . . . 18 class 𝑘
417, 34cop 4565 . . . . . . . . . . . . . . . . . . 19 class 𝑦, 𝑧
42 vw . . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
4342cv 1527 . . . . . . . . . . . . . . . . . . 19 class 𝑤
4441, 43, 12co 7145 . . . . . . . . . . . . . . . . . 18 class (⟨𝑦, 𝑧𝑜𝑤)
4540, 3, 44co 7145 . . . . . . . . . . . . . . . . 17 class (𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)
4632, 43, 12co 7145 . . . . . . . . . . . . . . . . 17 class (⟨𝑥, 𝑦𝑜𝑤)
4745, 5, 46co 7145 . . . . . . . . . . . . . . . 16 class ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓)
489, 34cop 4565 . . . . . . . . . . . . . . . . . 18 class 𝑥, 𝑧
4948, 43, 12co 7145 . . . . . . . . . . . . . . . . 17 class (⟨𝑥, 𝑧𝑜𝑤)
5040, 36, 49co 7145 . . . . . . . . . . . . . . . 16 class (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5147, 50wceq 1528 . . . . . . . . . . . . . . 15 wff ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5234, 43, 17co 7145 . . . . . . . . . . . . . . 15 class (𝑧𝑤)
5351, 39, 52wral 3138 . . . . . . . . . . . . . 14 wff 𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5453, 42, 28wral 3138 . . . . . . . . . . . . 13 wff 𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5538, 54wa 396 . . . . . . . . . . . 12 wff ((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
567, 34, 17co 7145 . . . . . . . . . . . 12 class (𝑦𝑧)
5755, 2, 56wral 3138 . . . . . . . . . . 11 wff 𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
5857, 4, 24wral 3138 . . . . . . . . . 10 wff 𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
5958, 33, 28wral 3138 . . . . . . . . 9 wff 𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
6059, 6, 28wral 3138 . . . . . . . 8 wff 𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
6131, 60wa 396 . . . . . . 7 wff (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
6261, 8, 28wral 3138 . . . . . 6 wff 𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
63 vc . . . . . . . 8 setvar 𝑐
6463cv 1527 . . . . . . 7 class 𝑐
65 cco 16567 . . . . . . 7 class comp
6664, 65cfv 6349 . . . . . 6 class (comp‘𝑐)
6762, 11, 66wsbc 3771 . . . . 5 wff [(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
68 chom 16566 . . . . . 6 class Hom
6964, 68cfv 6349 . . . . 5 class (Hom ‘𝑐)
7067, 16, 69wsbc 3771 . . . 4 wff [(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
71 cbs 16473 . . . . 5 class Base
7264, 71cfv 6349 . . . 4 class (Base‘𝑐)
7370, 27, 72wsbc 3771 . . 3 wff [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
7473, 63cab 2799 . 2 class {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
751, 74wceq 1528 1 wff Cat = {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
Colors of variables: wff setvar class
This definition is referenced by:  iscat  16933
  Copyright terms: Public domain W3C validator