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 = { 𝑐[ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ] [ ( comp ‘ 𝑐 ) / 𝑜 ]𝑥𝑏 ( ∃ 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦𝑏𝑧𝑏𝑓 ∈ ( 𝑥 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑧 ) ∧ ∀ 𝑤𝑏𝑘 ∈ ( 𝑧 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦𝑜 𝑧 ) 𝑓 ) ) ) ) }

Detailed syntax breakdown

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