Definition df-up 49527

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 49548), and can be generated from an existing universal pair by isomorphisms (upeu4 49549). See also oppcup 49560 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 49526	. 2 class UP
2		vd	. . 3 setvar 𝑑
3		ve	. . 3 setvar 𝑒
4		cvv 3442	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1541	. . . . 5 class 𝑑
7		cbs 17148	. . . . 5 class Base
8	6, 7	cfv 6500	. . . 4 class (Base‘𝑑)
9		vc	. . . . 5 setvar 𝑐
10	3	cv 1541	. . . . . 6 class 𝑒
11	10, 7	cfv 6500	. . . . 5 class (Base‘𝑒)
12		vh	. . . . . 6 setvar ℎ
13		chom 17200	. . . . . . 7 class Hom
14	6, 13	cfv 6500	. . . . . 6 class (Hom ‘𝑑)
15		vj	. . . . . . 7 setvar 𝑗
16	10, 13	cfv 6500	. . . . . . 7 class (Hom ‘𝑒)
17		vo	. . . . . . . 8 setvar 𝑜
18		cco 17201	. . . . . . . . 9 class comp
19	10, 18	cfv 6500	. . . . . . . 8 class (comp‘𝑒)
20		vf	. . . . . . . . 9 setvar 𝑓
21		vw	. . . . . . . . 9 setvar 𝑤
22		cfunc 17790	. . . . . . . . . 10 class Func
23	6, 10, 22	co 7368	. . . . . . . . 9 class (𝑑 Func 𝑒)
24	9	cv 1541	. . . . . . . . 9 class 𝑐
25		vx	. . . . . . . . . . . . 13 setvar 𝑥
26	25, 5	wel 2115	. . . . . . . . . . . 12 wff 𝑥 ∈ 𝑏
27		vm	. . . . . . . . . . . . . 14 setvar 𝑚
28	27	cv 1541	. . . . . . . . . . . . 13 class 𝑚
29	21	cv 1541	. . . . . . . . . . . . . 14 class 𝑤
30	25	cv 1541	. . . . . . . . . . . . . . 15 class 𝑥
31	20	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑓
32		c1st 7941	. . . . . . . . . . . . . . . 16 class 1st
33	31, 32	cfv 6500	. . . . . . . . . . . . . . 15 class (1st ‘𝑓)
34	30, 33	cfv 6500	. . . . . . . . . . . . . 14 class ((1st ‘𝑓)‘𝑥)
35	15	cv 1541	. . . . . . . . . . . . . 14 class 𝑗
36	29, 34, 35	co 7368	. . . . . . . . . . . . 13 class (𝑤𝑗((1st ‘𝑓)‘𝑥))
37	28, 36	wcel 2114	. . . . . . . . . . . 12 wff 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))
38	26, 37	wa 395	. . . . . . . . . . 11 wff (𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥)))
39		vg	. . . . . . . . . . . . . . . 16 setvar 𝑔
40	39	cv 1541	. . . . . . . . . . . . . . 15 class 𝑔
41		vk	. . . . . . . . . . . . . . . . . 18 setvar 𝑘
42	41	cv 1541	. . . . . . . . . . . . . . . . 17 class 𝑘
43		vy	. . . . . . . . . . . . . . . . . . 19 setvar 𝑦
44	43	cv 1541	. . . . . . . . . . . . . . . . . 18 class 𝑦
45		c2nd 7942	. . . . . . . . . . . . . . . . . . 19 class 2nd
46	31, 45	cfv 6500	. . . . . . . . . . . . . . . . . 18 class (2nd ‘𝑓)
47	30, 44, 46	co 7368	. . . . . . . . . . . . . . . . 17 class (𝑥(2nd ‘𝑓)𝑦)
48	42, 47	cfv 6500	. . . . . . . . . . . . . . . 16 class ((𝑥(2nd ‘𝑓)𝑦)‘𝑘)
49	29, 34	cop 4588	. . . . . . . . . . . . . . . . 17 class ⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩
50	44, 33	cfv 6500	. . . . . . . . . . . . . . . . 17 class ((1st ‘𝑓)‘𝑦)
51	17	cv 1541	. . . . . . . . . . . . . . . . 17 class 𝑜
52	49, 50, 51	co 7368	. . . . . . . . . . . . . . . 16 class (⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))
53	48, 28, 52	co 7368	. . . . . . . . . . . . . . 15 class (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
54	40, 53	wceq 1542	. . . . . . . . . . . . . 14 wff 𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
55	12	cv 1541	. . . . . . . . . . . . . . 15 class ℎ
56	30, 44, 55	co 7368	. . . . . . . . . . . . . 14 class (𝑥ℎ𝑦)
57	54, 41, 56	wreu 3350	. . . . . . . . . . . . 13 wff ∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
58	29, 50, 35	co 7368	. . . . . . . . . . . . 13 class (𝑤𝑗((1st ‘𝑓)‘𝑦))
59	57, 39, 58	wral 3052	. . . . . . . . . . . 12 wff ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
60	5	cv 1541	. . . . . . . . . . . 12 class 𝑏
61	59, 43, 60	wral 3052	. . . . . . . . . . 11 wff ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
62	38, 61	wa 395	. . . . . . . . . 10 wff ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))
63	62, 25, 27	copab 5162	. . . . . . . . 9 class {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}
64	20, 21, 23, 24, 63	cmpo 7370	. . . . . . . 8 class (𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
65	17, 19, 64	csb 3851	. . . . . . 7 class ⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
66	15, 16, 65	csb 3851	. . . . . 6 class ⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
67	12, 14, 66	csb 3851	. . . . 5 class ⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
68	9, 11, 67	csb 3851	. . . 4 class ⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
69	5, 8, 68	csb 3851	. . 3 class ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
70	2, 3, 4, 4, 69	cmpo 7370	. 2 class (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}))
71	1, 70	wceq 1542	1 wff UP = (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}))

This definition is referenced by:  reldmup  49528  upfval  49529