Definition df-up 50226

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 50247), and can be generated from an existing universal pair by isomorphisms (upeu4 50248). See also oppcup 50259 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 50225	. 2 class UP
2		vd	. . 3 setvar 𝑑
3		ve	. . 3 setvar 𝑒
4		cvv 3451	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1569	. . . . 5 class 𝑑
7		cbs 17367	. . . . 5 class Base
8	6, 7	cfv 6531	. . . 4 class (Base‘𝑑)
9		vc	. . . . 5 setvar 𝑐
10	3	cv 1569	. . . . . 6 class 𝑒
11	10, 7	cfv 6531	. . . . 5 class (Base‘𝑒)
12		vh	. . . . . 6 setvar ℎ
13		chom 17419	. . . . . . 7 class Hom
14	6, 13	cfv 6531	. . . . . 6 class (Hom ‘𝑑)
15		vj	. . . . . . 7 setvar 𝑗
16	10, 13	cfv 6531	. . . . . . 7 class (Hom ‘𝑒)
17		vo	. . . . . . . 8 setvar 𝑜
18		cco 17420	. . . . . . . . 9 class comp
19	10, 18	cfv 6531	. . . . . . . 8 class (comp‘𝑒)
20		vf	. . . . . . . . 9 setvar 𝑓
21		vw	. . . . . . . . 9 setvar 𝑤
22		cfunc 18009	. . . . . . . . . 10 class Func
23	6, 10, 22	co 7412	. . . . . . . . 9 class (𝑑 Func 𝑒)
24	9	cv 1569	. . . . . . . . 9 class 𝑐
25		vx	. . . . . . . . . . . . 13 setvar 𝑥
26	25, 5	wel 2146	. . . . . . . . . . . 12 wff 𝑥 ∈ 𝑏
27		vm	. . . . . . . . . . . . . 14 setvar 𝑚
28	27	cv 1569	. . . . . . . . . . . . 13 class 𝑚
29	21	cv 1569	. . . . . . . . . . . . . 14 class 𝑤
30	25	cv 1569	. . . . . . . . . . . . . . 15 class 𝑥
31	20	cv 1569	. . . . . . . . . . . . . . . 16 class 𝑓
32		c1st 7988	. . . . . . . . . . . . . . . 16 class 1st
33	31, 32	cfv 6531	. . . . . . . . . . . . . . 15 class (1st ‘𝑓)
34	30, 33	cfv 6531	. . . . . . . . . . . . . 14 class ((1st ‘𝑓)‘𝑥)
35	15	cv 1569	. . . . . . . . . . . . . 14 class 𝑗
36	29, 34, 35	co 7412	. . . . . . . . . . . . 13 class (𝑤𝑗((1st ‘𝑓)‘𝑥))
37	28, 36	wcel 2145	. . . . . . . . . . . 12 wff 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))
38	26, 37	wa 401	. . . . . . . . . . 11 wff (𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥)))
39		vg	. . . . . . . . . . . . . . . 16 setvar 𝑔
40	39	cv 1569	. . . . . . . . . . . . . . 15 class 𝑔
41		vk	. . . . . . . . . . . . . . . . . 18 setvar 𝑘
42	41	cv 1569	. . . . . . . . . . . . . . . . 17 class 𝑘
43		vy	. . . . . . . . . . . . . . . . . . 19 setvar 𝑦
44	43	cv 1569	. . . . . . . . . . . . . . . . . 18 class 𝑦
45		c2nd 7989	. . . . . . . . . . . . . . . . . . 19 class 2nd
46	31, 45	cfv 6531	. . . . . . . . . . . . . . . . . 18 class (2nd ‘𝑓)
47	30, 44, 46	co 7412	. . . . . . . . . . . . . . . . 17 class (𝑥(2nd ‘𝑓)𝑦)
48	42, 47	cfv 6531	. . . . . . . . . . . . . . . 16 class ((𝑥(2nd ‘𝑓)𝑦)‘𝑘)
49	29, 34	cop 4590	. . . . . . . . . . . . . . . . 17 class ⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩
50	44, 33	cfv 6531	. . . . . . . . . . . . . . . . 17 class ((1st ‘𝑓)‘𝑦)
51	17	cv 1569	. . . . . . . . . . . . . . . . 17 class 𝑜
52	49, 50, 51	co 7412	. . . . . . . . . . . . . . . 16 class (⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))
53	48, 28, 52	co 7412	. . . . . . . . . . . . . . 15 class (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
54	40, 53	wceq 1570	. . . . . . . . . . . . . 14 wff 𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
55	12	cv 1569	. . . . . . . . . . . . . . 15 class ℎ
56	30, 44, 55	co 7412	. . . . . . . . . . . . . 14 class (𝑥ℎ𝑦)
57	54, 41, 56	wreu 3364	. . . . . . . . . . . . 13 wff ∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
58	29, 50, 35	co 7412	. . . . . . . . . . . . 13 class (𝑤𝑗((1st ‘𝑓)‘𝑦))
59	57, 39, 58	wral 3077	. . . . . . . . . . . 12 wff ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
60	5	cv 1569	. . . . . . . . . . . 12 class 𝑏
61	59, 43, 60	wral 3077	. . . . . . . . . . 11 wff ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
62	38, 61	wa 401	. . . . . . . . . 10 wff ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))
63	62, 25, 27	copab 5167	. . . . . . . . 9 class {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}
64	20, 21, 23, 24, 63	cmpo 7414	. . . . . . . 8 class (𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
65	17, 19, 64	csb 3847	. . . . . . 7 class ⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
66	15, 16, 65	csb 3847	. . . . . 6 class ⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
67	12, 14, 66	csb 3847	. . . . 5 class ⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
68	9, 11, 67	csb 3847	. . . 4 class ⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
69	5, 8, 68	csb 3847	. . 3 class ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
70	2, 3, 4, 4, 69	cmpo 7414	. 2 class (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}))
71	1, 70	wceq 1570	1 wff UP = (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}))

This definition is used by:  reldmup  50227  upfval  50228