Definition df-up 49661

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 49682), and can be generated from an existing universal pair by isomorphisms (upeu4 49683). See also oppcup 49694 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 49660	. 2 class UP
2		vd	. . 3 setvar 𝑑
3		ve	. . 3 setvar 𝑒
4		cvv 3430	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1541	. . . . 5 class 𝑑
7		cbs 17170	. . . . 5 class Base
8	6, 7	cfv 6492	. . . 4 class (Base‘𝑑)
9		vc	. . . . 5 setvar 𝑐
10	3	cv 1541	. . . . . 6 class 𝑒
11	10, 7	cfv 6492	. . . . 5 class (Base‘𝑒)
12		vh	. . . . . 6 setvar ℎ
13		chom 17222	. . . . . . 7 class Hom
14	6, 13	cfv 6492	. . . . . 6 class (Hom ‘𝑑)
15		vj	. . . . . . 7 setvar 𝑗
16	10, 13	cfv 6492	. . . . . . 7 class (Hom ‘𝑒)
17		vo	. . . . . . . 8 setvar 𝑜
18		cco 17223	. . . . . . . . 9 class comp
19	10, 18	cfv 6492	. . . . . . . 8 class (comp‘𝑒)
20		vf	. . . . . . . . 9 setvar 𝑓
21		vw	. . . . . . . . 9 setvar 𝑤
22		cfunc 17812	. . . . . . . . . 10 class Func
23	6, 10, 22	co 7360	. . . . . . . . 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 7933	. . . . . . . . . . . . . . . 16 class 1st
33	31, 32	cfv 6492	. . . . . . . . . . . . . . 15 class (1st ‘𝑓)
34	30, 33	cfv 6492	. . . . . . . . . . . . . 14 class ((1st ‘𝑓)‘𝑥)
35	15	cv 1541	. . . . . . . . . . . . . 14 class 𝑗
36	29, 34, 35	co 7360	. . . . . . . . . . . . 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 7934	. . . . . . . . . . . . . . . . . . 19 class 2nd
46	31, 45	cfv 6492	. . . . . . . . . . . . . . . . . 18 class (2nd ‘𝑓)
47	30, 44, 46	co 7360	. . . . . . . . . . . . . . . . 17 class (𝑥(2nd ‘𝑓)𝑦)
48	42, 47	cfv 6492	. . . . . . . . . . . . . . . 16 class ((𝑥(2nd ‘𝑓)𝑦)‘𝑘)
49	29, 34	cop 4574	. . . . . . . . . . . . . . . . 17 class ⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩
50	44, 33	cfv 6492	. . . . . . . . . . . . . . . . 17 class ((1st ‘𝑓)‘𝑦)
51	17	cv 1541	. . . . . . . . . . . . . . . . 17 class 𝑜
52	49, 50, 51	co 7360	. . . . . . . . . . . . . . . 16 class (⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))
53	48, 28, 52	co 7360	. . . . . . . . . . . . . . 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 7360	. . . . . . . . . . . . . 14 class (𝑥ℎ𝑦)
57	54, 41, 56	wreu 3341	. . . . . . . . . . . . 13 wff ∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
58	29, 50, 35	co 7360	. . . . . . . . . . . . 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 5148	. . . . . . . . 9 class {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}
64	20, 21, 23, 24, 63	cmpo 7362	. . . . . . . 8 class (𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
65	17, 19, 64	csb 3838	. . . . . . 7 class ⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
66	15, 16, 65	csb 3838	. . . . . 6 class ⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
67	12, 14, 66	csb 3838	. . . . 5 class ⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
68	9, 11, 67	csb 3838	. . . 4 class ⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
69	5, 8, 68	csb 3838	. . 3 class ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
70	2, 3, 4, 4, 69	cmpo 7362	. 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  49662  upfval  49663