Definition df-up 49759

Description: Definition of the class of universal properties.

Given categories 𝐷 and 𝐸, if 𝐹:𝐷⟶𝐸 is a functor and 𝑊 an object of 𝐸, a universal pair from 𝑊 to 𝐹 is a pair ⟨𝑋, 𝑀⟩ consisting of an object 𝑋 of 𝐷 and a morphism 𝑀:𝑊⟶𝐹𝑋 of 𝐸, such that to every pair ⟨𝑦, 𝑔⟩ with 𝑦 an object of 𝐷 and 𝑔:𝑊⟶𝐹𝑦 a morphism of 𝐸, there is a unique morphism 𝑘:𝑋⟶𝑦 of 𝐷 with 𝐹𝑘 ⚬ 𝑀 = 𝑔. Such property is commonly referred to as a universal property. In our definition, it is denoted as 𝑋(𝐹(𝐷 UP 𝐸)𝑊)𝑀.

Note that the universal pair is termed differently as "universal arrow" in p. 55 of Mac Lane, Saunders, Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf (retrieved 6 Oct 2025). Interestingly, the "universal arrow" is referring to the morphism 𝑀 instead of the pair near the end of the same piece of the text, causing name collision. The name "universal arrow" is also adopted in papers such as https://arxiv.org/pdf/2212.08981. Alternatively, the universal pair is called the "universal morphism" in Wikipedia (https://en.wikipedia.org/wiki/Universal_property) as well as published works, e.g., https://arxiv.org/pdf/2412.12179. But the pair ⟨𝑋, 𝑀⟩ should be named differently as the morphism 𝑀, and thus we call 𝑋 the universal object, 𝑀 the universal morphism, and ⟨𝑋, 𝑀⟩ the universal pair.

Given its existence, such universal pair is essentially unique (upeu3 49780), and can be generated from an existing universal pair by isomorphisms (upeu4 49781). See also oppcup 49792 for the dual concept.

(Contributed by Zhi Wang, 24-Sep-2025.)

Assertion

Ref	Expression
df-up	⊢ UP = (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}))

Distinct variable group:   𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑗,𝑘,𝑚,𝑜,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-up

Step	Hyp	Ref	Expression
1		cup 49758	. 2 class UP
2		vd	. . 3 setvar 𝑑
3		ve	. . 3 setvar 𝑒
4		cvv 3453	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1558	. . . . 5 class 𝑑
7		cbs 17228	. . . . 5 class Base
8	6, 7	cfv 6517	. . . 4 class (Base‘𝑑)
9		vc	. . . . 5 setvar 𝑐
10	3	cv 1558	. . . . . 6 class 𝑒
11	10, 7	cfv 6517	. . . . 5 class (Base‘𝑒)
12		vh	. . . . . 6 setvar ℎ
13		chom 17280	. . . . . . 7 class Hom
14	6, 13	cfv 6517	. . . . . 6 class (Hom ‘𝑑)
15		vj	. . . . . . 7 setvar 𝑗
16	10, 13	cfv 6517	. . . . . . 7 class (Hom ‘𝑒)
17		vo	. . . . . . . 8 setvar 𝑜
18		cco 17281	. . . . . . . . 9 class comp
19	10, 18	cfv 6517	. . . . . . . 8 class (comp‘𝑒)
20		vf	. . . . . . . . 9 setvar 𝑓
21		vw	. . . . . . . . 9 setvar 𝑤
22		cfunc 17870	. . . . . . . . . 10 class Func
23	6, 10, 22	co 7392	. . . . . . . . 9 class (𝑑 Func 𝑒)
24	9	cv 1558	. . . . . . . . 9 class 𝑐
25		vx	. . . . . . . . . . . . 13 setvar 𝑥
26	25, 5	wel 2142	. . . . . . . . . . . 12 wff 𝑥 ∈ 𝑏
27		vm	. . . . . . . . . . . . . 14 setvar 𝑚
28	27	cv 1558	. . . . . . . . . . . . 13 class 𝑚
29	21	cv 1558	. . . . . . . . . . . . . 14 class 𝑤
30	25	cv 1558	. . . . . . . . . . . . . . 15 class 𝑥
31	20	cv 1558	. . . . . . . . . . . . . . . 16 class 𝑓
32		c1st 7964	. . . . . . . . . . . . . . . 16 class 1st
33	31, 32	cfv 6517	. . . . . . . . . . . . . . 15 class (1st ‘𝑓)
34	30, 33	cfv 6517	. . . . . . . . . . . . . 14 class ((1st ‘𝑓)‘𝑥)
35	15	cv 1558	. . . . . . . . . . . . . 14 class 𝑗
36	29, 34, 35	co 7392	. . . . . . . . . . . . 13 class (𝑤𝑗((1st ‘𝑓)‘𝑥))
37	28, 36	wcel 2141	. . . . . . . . . . . 12 wff 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))
38	26, 37	wa 399	. . . . . . . . . . 11 wff (𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥)))
39		vg	. . . . . . . . . . . . . . . 16 setvar 𝑔
40	39	cv 1558	. . . . . . . . . . . . . . 15 class 𝑔
41		vk	. . . . . . . . . . . . . . . . . 18 setvar 𝑘
42	41	cv 1558	. . . . . . . . . . . . . . . . 17 class 𝑘
43		vy	. . . . . . . . . . . . . . . . . . 19 setvar 𝑦
44	43	cv 1558	. . . . . . . . . . . . . . . . . 18 class 𝑦
45		c2nd 7965	. . . . . . . . . . . . . . . . . . 19 class 2nd
46	31, 45	cfv 6517	. . . . . . . . . . . . . . . . . 18 class (2nd ‘𝑓)
47	30, 44, 46	co 7392	. . . . . . . . . . . . . . . . 17 class (𝑥(2nd ‘𝑓)𝑦)
48	42, 47	cfv 6517	. . . . . . . . . . . . . . . 16 class ((𝑥(2nd ‘𝑓)𝑦)‘𝑘)
49	29, 34	cop 4587	. . . . . . . . . . . . . . . . 17 class ⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩
50	44, 33	cfv 6517	. . . . . . . . . . . . . . . . 17 class ((1st ‘𝑓)‘𝑦)
51	17	cv 1558	. . . . . . . . . . . . . . . . 17 class 𝑜
52	49, 50, 51	co 7392	. . . . . . . . . . . . . . . 16 class (⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))
53	48, 28, 52	co 7392	. . . . . . . . . . . . . . 15 class (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
54	40, 53	wceq 1559	. . . . . . . . . . . . . 14 wff 𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
55	12	cv 1558	. . . . . . . . . . . . . . 15 class ℎ
56	30, 44, 55	co 7392	. . . . . . . . . . . . . 14 class (𝑥ℎ𝑦)
57	54, 41, 56	wreu 3364	. . . . . . . . . . . . 13 wff ∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
58	29, 50, 35	co 7392	. . . . . . . . . . . . 13 class (𝑤𝑗((1st ‘𝑓)‘𝑦))
59	57, 39, 58	wral 3075	. . . . . . . . . . . 12 wff ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
60	5	cv 1558	. . . . . . . . . . . 12 class 𝑏
61	59, 43, 60	wral 3075	. . . . . . . . . . 11 wff ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
62	38, 61	wa 399	. . . . . . . . . 10 wff ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))
63	62, 25, 27	copab 5161	. . . . . . . . 9 class {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}
64	20, 21, 23, 24, 63	cmpo 7394	. . . . . . . 8 class (𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
65	17, 19, 64	csb 3852	. . . . . . 7 class ⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
66	15, 16, 65	csb 3852	. . . . . 6 class ⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
67	12, 14, 66	csb 3852	. . . . 5 class ⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
68	9, 11, 67	csb 3852	. . . 4 class ⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
69	5, 8, 68	csb 3852	. . 3 class ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
70	2, 3, 4, 4, 69	cmpo 7394	. 2 class (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}))
71	1, 70	wceq 1559	1 wff UP = (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}))

This definition is referenced by:  reldmup  49760  upfval  49761