Metamath Proof Explorer

Definition df-cat

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 ). See setc2obas and setc2ohom 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" ( ( Basec ) ), the morphisms "hom" ( ( Homc ) ) and the composition law "o" ( ( compc ) ). 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 . (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007) (Revised by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-cat ⊢ Cat = c | [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ [˙ comp ⁡ c / o]˙ ∀ x ∈ b ∃ g ∈ x h x ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∧ ∀ y ∈ b ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccat class Cat
1 vc setvar c
2 cbs class Base
3 1 cv setvar c
4 3 2 cfv class Base c
5 vb setvar b
6 chom class Hom
7 3 6 cfv class Hom ⁡ c
8 vh setvar h
9 cco class comp
10 3 9 cfv class comp ⁡ c
11 vo setvar o
12 vx setvar x
13 5 cv setvar b
14 vg setvar g
15 12 cv setvar x
16 8 cv setvar h
17 15 15 16 co class x h x
18 vy setvar y
19 vf setvar f
20 18 cv setvar y
21 20 15 16 co class y h x
22 14 cv setvar g
23 20 15 cop class y x
24 11 cv setvar o
25 23 15 24 co class y x o x
26 19 cv setvar f
27 22 26 25 co class g y x o x f
28 27 26 wceq wff g y x o x f = f
29 28 19 21 wral wff ∀ f ∈ y h x g y x o x f = f
30 15 20 16 co class x h y
31 15 15 cop class x x
32 31 20 24 co class x x o y
33 26 22 32 co class f x x o y g
34 33 26 wceq wff f x x o y g = f
35 34 19 30 wral wff ∀ f ∈ x h y f x x o y g = f
36 29 35 wa wff ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
37 36 18 13 wral wff ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
38 37 14 17 wrex wff ∃ g ∈ x h x ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
39 vz setvar z
40 39 cv setvar z
41 20 40 16 co class y h z
42 15 20 cop class x y
43 42 40 24 co class x y o z
44 22 26 43 co class g x y o z f
45 15 40 16 co class x h z
46 44 45 wcel wff g x y o z f ∈ x h z
47 vw setvar w
48 vk setvar k
49 47 cv setvar w
50 40 49 16 co class z h w
51 48 cv setvar k
52 20 40 cop class y z
53 52 49 24 co class y z o w
54 51 22 53 co class k y z o w g
55 42 49 24 co class x y o w
56 54 26 55 co class k y z o w g x y o w f
57 15 40 cop class x z
58 57 49 24 co class x z o w
59 51 44 58 co class k x z o w g x y o z f
60 56 59 wceq wff k y z o w g x y o w f = k x z o w g x y o z f
61 60 48 50 wral wff ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
62 61 47 13 wral wff ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
63 46 62 wa wff g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
64 63 14 41 wral wff ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
65 64 19 30 wral wff ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
66 65 39 13 wral wff ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
67 66 18 13 wral wff ∀ y ∈ b ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
68 38 67 wa wff ∃ g ∈ x h x ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∧ ∀ y ∈ b ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
69 68 12 13 wral wff ∀ x ∈ b ∃ g ∈ x h x ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∧ ∀ y ∈ b ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
70 69 11 10 wsbc wff [˙ comp ⁡ c / o]˙ ∀ x ∈ b ∃ g ∈ x h x ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∧ ∀ y ∈ b ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
71 70 8 7 wsbc wff [˙ Hom ⁡ c / h]˙ [˙ comp ⁡ c / o]˙ ∀ x ∈ b ∃ g ∈ x h x ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∧ ∀ y ∈ b ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
72 71 5 4 wsbc wff [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ [˙ comp ⁡ c / o]˙ ∀ x ∈ b ∃ g ∈ x h x ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∧ ∀ y ∈ b ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
73 72 1 cab class c | [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ [˙ comp ⁡ c / o]˙ ∀ x ∈ b ∃ g ∈ x h x ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∧ ∀ y ∈ b ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f
74 0 73 wceq wff Cat = c | [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ [˙ comp ⁡ c / o]˙ ∀ x ∈ b ∃ g ∈ x h x ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∧ ∀ y ∈ b ∀ z ∈ b ∀ f ∈ x h y ∀ g ∈ y h z g x y o z f ∈ x h z ∧ ∀ w ∈ b ∀ k ∈ z h w k y z o w g x y o w f = k x z o w g x y o z f