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 17651
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, without the axiom CAT 1, i.e., pairwise disjointness of hom-sets (cat1 18089). See setc2obas 18086 and setc2ohom 18087 for a counterexample. 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 17652. (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 17647 . 2 class Cat
2 vg . . . . . . . . . . . . . . 15 setvar 𝑔
32cv 1532 . . . . . . . . . . . . . 14 class 𝑔
4 vf . . . . . . . . . . . . . . 15 setvar 𝑓
54cv 1532 . . . . . . . . . . . . . 14 class 𝑓
6 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
76cv 1532 . . . . . . . . . . . . . . . 16 class 𝑦
8 vx . . . . . . . . . . . . . . . . 17 setvar 𝑥
98cv 1532 . . . . . . . . . . . . . . . 16 class 𝑥
107, 9cop 4636 . . . . . . . . . . . . . . 15 class 𝑦, 𝑥
11 vo . . . . . . . . . . . . . . . 16 setvar 𝑜
1211cv 1532 . . . . . . . . . . . . . . 15 class 𝑜
1310, 9, 12co 7419 . . . . . . . . . . . . . 14 class (⟨𝑦, 𝑥𝑜𝑥)
143, 5, 13co 7419 . . . . . . . . . . . . 13 class (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓)
1514, 5wceq 1533 . . . . . . . . . . . 12 wff (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
16 vh . . . . . . . . . . . . . 14 setvar
1716cv 1532 . . . . . . . . . . . . 13 class
187, 9, 17co 7419 . . . . . . . . . . . 12 class (𝑦𝑥)
1915, 4, 18wral 3050 . . . . . . . . . . 11 wff 𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
209, 9cop 4636 . . . . . . . . . . . . . . 15 class 𝑥, 𝑥
2120, 7, 12co 7419 . . . . . . . . . . . . . 14 class (⟨𝑥, 𝑥𝑜𝑦)
225, 3, 21co 7419 . . . . . . . . . . . . 13 class (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔)
2322, 5wceq 1533 . . . . . . . . . . . 12 wff (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
249, 7, 17co 7419 . . . . . . . . . . . 12 class (𝑥𝑦)
2523, 4, 24wral 3050 . . . . . . . . . . 11 wff 𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
2619, 25wa 394 . . . . . . . . . 10 wff (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
27 vb . . . . . . . . . . 11 setvar 𝑏
2827cv 1532 . . . . . . . . . 10 class 𝑏
2926, 6, 28wral 3050 . . . . . . . . 9 wff 𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
309, 9, 17co 7419 . . . . . . . . 9 class (𝑥𝑥)
3129, 2, 30wrex 3059 . . . . . . . 8 wff 𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
329, 7cop 4636 . . . . . . . . . . . . . . . 16 class 𝑥, 𝑦
33 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
3433cv 1532 . . . . . . . . . . . . . . . 16 class 𝑧
3532, 34, 12co 7419 . . . . . . . . . . . . . . 15 class (⟨𝑥, 𝑦𝑜𝑧)
363, 5, 35co 7419 . . . . . . . . . . . . . 14 class (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)
379, 34, 17co 7419 . . . . . . . . . . . . . 14 class (𝑥𝑧)
3836, 37wcel 2098 . . . . . . . . . . . . 13 wff (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧)
39 vk . . . . . . . . . . . . . . . . . . 19 setvar 𝑘
4039cv 1532 . . . . . . . . . . . . . . . . . 18 class 𝑘
417, 34cop 4636 . . . . . . . . . . . . . . . . . . 19 class 𝑦, 𝑧
42 vw . . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
4342cv 1532 . . . . . . . . . . . . . . . . . . 19 class 𝑤
4441, 43, 12co 7419 . . . . . . . . . . . . . . . . . 18 class (⟨𝑦, 𝑧𝑜𝑤)
4540, 3, 44co 7419 . . . . . . . . . . . . . . . . 17 class (𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)
4632, 43, 12co 7419 . . . . . . . . . . . . . . . . 17 class (⟨𝑥, 𝑦𝑜𝑤)
4745, 5, 46co 7419 . . . . . . . . . . . . . . . 16 class ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓)
489, 34cop 4636 . . . . . . . . . . . . . . . . . 18 class 𝑥, 𝑧
4948, 43, 12co 7419 . . . . . . . . . . . . . . . . 17 class (⟨𝑥, 𝑧𝑜𝑤)
5040, 36, 49co 7419 . . . . . . . . . . . . . . . 16 class (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5147, 50wceq 1533 . . . . . . . . . . . . . . 15 wff ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5234, 43, 17co 7419 . . . . . . . . . . . . . . 15 class (𝑧𝑤)
5351, 39, 52wral 3050 . . . . . . . . . . . . . 14 wff 𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5453, 42, 28wral 3050 . . . . . . . . . . . . 13 wff 𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))
5538, 54wa 394 . . . . . . . . . . . 12 wff ((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
567, 34, 17co 7419 . . . . . . . . . . . 12 class (𝑦𝑧)
5755, 2, 56wral 3050 . . . . . . . . . . 11 wff 𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
5857, 4, 24wral 3050 . . . . . . . . . 10 wff 𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
5958, 33, 28wral 3050 . . . . . . . . 9 wff 𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
6059, 6, 28wral 3050 . . . . . . . 8 wff 𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))
6131, 60wa 394 . . . . . . 7 wff (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
6261, 8, 28wral 3050 . . . . . 6 wff 𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
63 vc . . . . . . . 8 setvar 𝑐
6463cv 1532 . . . . . . 7 class 𝑐
65 cco 17248 . . . . . . 7 class comp
6664, 65cfv 6549 . . . . . 6 class (comp‘𝑐)
6762, 11, 66wsbc 3773 . . . . 5 wff [(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
68 chom 17247 . . . . . 6 class Hom
6964, 68cfv 6549 . . . . 5 class (Hom ‘𝑐)
7067, 16, 69wsbc 3773 . . . 4 wff [(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
71 cbs 17183 . . . . 5 class Base
7264, 71cfv 6549 . . . 4 class (Base‘𝑐)
7370, 27, 72wsbc 3773 . . 3 wff [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))
7473, 63cab 2702 . 2 class {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
751, 74wceq 1533 1 wff Cat = {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
Colors of variables: wff setvar class
This definition is referenced by:  iscat  17655
  Copyright terms: Public domain W3C validator