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