Definition df-cat 16931

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 16932. (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

Step	Hyp	Ref	Expression
1		ccat 16927	. 2 class Cat
2		vg	. . . . . . . . . . . . . . 15 setvar 𝑔
3	2	cv 1537	. . . . . . . . . . . . . 14 class 𝑔
4		vf	. . . . . . . . . . . . . . 15 setvar 𝑓
5	4	cv 1537	. . . . . . . . . . . . . 14 class 𝑓
6		vy	. . . . . . . . . . . . . . . . 17 setvar 𝑦
7	6	cv 1537	. . . . . . . . . . . . . . . 16 class 𝑦
8		vx	. . . . . . . . . . . . . . . . 17 setvar 𝑥
9	8	cv 1537	. . . . . . . . . . . . . . . 16 class 𝑥
10	7, 9	cop 4531	. . . . . . . . . . . . . . 15 class ⟨𝑦, 𝑥⟩
11		vo	. . . . . . . . . . . . . . . 16 setvar 𝑜
12	11	cv 1537	. . . . . . . . . . . . . . 15 class 𝑜
13	10, 9, 12	co 7135	. . . . . . . . . . . . . 14 class (⟨𝑦, 𝑥⟩𝑜𝑥)
14	3, 5, 13	co 7135	. . . . . . . . . . . . 13 class (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓)
15	14, 5	wceq 1538	. . . . . . . . . . . 12 wff (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
16		vh	. . . . . . . . . . . . . 14 setvar ℎ
17	16	cv 1537	. . . . . . . . . . . . 13 class ℎ
18	7, 9, 17	co 7135	. . . . . . . . . . . 12 class (𝑦ℎ𝑥)
19	15, 4, 18	wral 3106	. . . . . . . . . . 11 wff ∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
20	9, 9	cop 4531	. . . . . . . . . . . . . . 15 class ⟨𝑥, 𝑥⟩
21	20, 7, 12	co 7135	. . . . . . . . . . . . . 14 class (⟨𝑥, 𝑥⟩𝑜𝑦)
22	5, 3, 21	co 7135	. . . . . . . . . . . . 13 class (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔)
23	22, 5	wceq 1538	. . . . . . . . . . . 12 wff (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
24	9, 7, 17	co 7135	. . . . . . . . . . . 12 class (𝑥ℎ𝑦)
25	23, 4, 24	wral 3106	. . . . . . . . . . 11 wff ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
26	19, 25	wa 399	. . . . . . . . . 10 wff (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
27		vb	. . . . . . . . . . 11 setvar 𝑏
28	27	cv 1537	. . . . . . . . . 10 class 𝑏
29	26, 6, 28	wral 3106	. . . . . . . . 9 wff ∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
30	9, 9, 17	co 7135	. . . . . . . . 9 class (𝑥ℎ𝑥)
31	29, 2, 30	wrex 3107	. . . . . . . 8 wff ∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
32	9, 7	cop 4531	. . . . . . . . . . . . . . . 16 class ⟨𝑥, 𝑦⟩
33		vz	. . . . . . . . . . . . . . . . 17 setvar 𝑧
34	33	cv 1537	. . . . . . . . . . . . . . . 16 class 𝑧
35	32, 34, 12	co 7135	. . . . . . . . . . . . . . 15 class (⟨𝑥, 𝑦⟩𝑜𝑧)
36	3, 5, 35	co 7135	. . . . . . . . . . . . . 14 class (𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓)
37	9, 34, 17	co 7135	. . . . . . . . . . . . . 14 class (𝑥ℎ𝑧)
38	36, 37	wcel 2111	. . . . . . . . . . . . 13 wff (𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧)
39		vk	. . . . . . . . . . . . . . . . . . 19 setvar 𝑘
40	39	cv 1537	. . . . . . . . . . . . . . . . . 18 class 𝑘
41	7, 34	cop 4531	. . . . . . . . . . . . . . . . . . 19 class ⟨𝑦, 𝑧⟩
42		vw	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
43	42	cv 1537	. . . . . . . . . . . . . . . . . . 19 class 𝑤
44	41, 43, 12	co 7135	. . . . . . . . . . . . . . . . . 18 class (⟨𝑦, 𝑧⟩𝑜𝑤)
45	40, 3, 44	co 7135	. . . . . . . . . . . . . . . . 17 class (𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)
46	32, 43, 12	co 7135	. . . . . . . . . . . . . . . . 17 class (⟨𝑥, 𝑦⟩𝑜𝑤)
47	45, 5, 46	co 7135	. . . . . . . . . . . . . . . 16 class ((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓)
48	9, 34	cop 4531	. . . . . . . . . . . . . . . . . 18 class ⟨𝑥, 𝑧⟩
49	48, 43, 12	co 7135	. . . . . . . . . . . . . . . . 17 class (⟨𝑥, 𝑧⟩𝑜𝑤)
50	40, 36, 49	co 7135	. . . . . . . . . . . . . . . 16 class (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))
51	47, 50	wceq 1538	. . . . . . . . . . . . . . 15 wff ((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))
52	34, 43, 17	co 7135	. . . . . . . . . . . . . . 15 class (𝑧ℎ𝑤)
53	51, 39, 52	wral 3106	. . . . . . . . . . . . . 14 wff ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))
54	53, 42, 28	wral 3106	. . . . . . . . . . . . 13 wff ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))
55	38, 54	wa 399	. . . . . . . . . . . 12 wff ((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓)))
56	7, 34, 17	co 7135	. . . . . . . . . . . 12 class (𝑦ℎ𝑧)
57	55, 2, 56	wral 3106	. . . . . . . . . . 11 wff ∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓)))
58	57, 4, 24	wral 3106	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓)))
59	58, 33, 28	wral 3106	. . . . . . . . 9 wff ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓)))
60	59, 6, 28	wral 3106	. . . . . . . 8 wff ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓)))
61	31, 60	wa 399	. . . . . . 7 wff (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))))
62	61, 8, 28	wral 3106	. . . . . 6 wff ∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))))
63		vc	. . . . . . . 8 setvar 𝑐
64	63	cv 1537	. . . . . . 7 class 𝑐
65		cco 16569	. . . . . . 7 class comp
66	64, 65	cfv 6324	. . . . . 6 class (comp‘𝑐)
67	62, 11, 66	wsbc 3720	. . . . 5 wff [(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))))
68		chom 16568	. . . . . 6 class Hom
69	64, 68	cfv 6324	. . . . 5 class (Hom ‘𝑐)
70	67, 16, 69	wsbc 3720	. . . 4 wff [(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))))
71		cbs 16475	. . . . 5 class Base
72	64, 71	cfv 6324	. . . 4 class (Base‘𝑐)
73	70, 27, 72	wsbc 3720	. . 3 wff [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))))
74	73, 63	cab 2776	. 2 class {𝑐 ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))))}
75	1, 74	wceq 1538	1 wff Cat = {𝑐 ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(⟨𝑦, 𝑧⟩𝑜𝑤)𝑔)(⟨𝑥, 𝑦⟩𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩𝑜𝑤)(𝑔(⟨𝑥, 𝑦⟩𝑜𝑧)𝑓))))}

This definition is referenced by:  iscat  16935