Definition df-up 49993

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 50014), and can be generated from an existing universal pair by isomorphisms (upeu4 50015). See also oppcup 50026 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 49992	. 2 class UP
2		vd	. . 3 setvar 𝑑
3		ve	. . 3 setvar 𝑒
4		cvv 3458	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1569	. . . . 5 class 𝑑
7		cbs 17294	. . . . 5 class Base
8	6, 7	cfv 6543	. . . 4 class (Base‘𝑑)
9		vc	. . . . 5 setvar 𝑐
10	3	cv 1569	. . . . . 6 class 𝑒
11	10, 7	cfv 6543	. . . . 5 class (Base‘𝑒)
12		vh	. . . . . 6 setvar ℎ
13		chom 17346	. . . . . . 7 class Hom
14	6, 13	cfv 6543	. . . . . 6 class (Hom ‘𝑑)
15		vj	. . . . . . 7 setvar 𝑗
16	10, 13	cfv 6543	. . . . . . 7 class (Hom ‘𝑒)
17		vo	. . . . . . . 8 setvar 𝑜
18		cco 17347	. . . . . . . . 9 class comp
19	10, 18	cfv 6543	. . . . . . . 8 class (comp‘𝑒)
20		vf	. . . . . . . . 9 setvar 𝑓
21		vw	. . . . . . . . 9 setvar 𝑤
22		cfunc 17936	. . . . . . . . . 10 class Func
23	6, 10, 22	co 7423	. . . . . . . . 9 class (𝑑 Func 𝑒)
24	9	cv 1569	. . . . . . . . 9 class 𝑐
25		vx	. . . . . . . . . . . . 13 setvar 𝑥
26	25, 5	wel 2147	. . . . . . . . . . . 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 7993	. . . . . . . . . . . . . . . 16 class 1st
33	31, 32	cfv 6543	. . . . . . . . . . . . . . 15 class (1st ‘𝑓)
34	30, 33	cfv 6543	. . . . . . . . . . . . . 14 class ((1st ‘𝑓)‘𝑥)
35	15	cv 1569	. . . . . . . . . . . . . 14 class 𝑗
36	29, 34, 35	co 7423	. . . . . . . . . . . . 13 class (𝑤𝑗((1st ‘𝑓)‘𝑥))
37	28, 36	wcel 2146	. . . . . . . . . . . 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 7994	. . . . . . . . . . . . . . . . . . 19 class 2nd
46	31, 45	cfv 6543	. . . . . . . . . . . . . . . . . 18 class (2nd ‘𝑓)
47	30, 44, 46	co 7423	. . . . . . . . . . . . . . . . 17 class (𝑥(2nd ‘𝑓)𝑦)
48	42, 47	cfv 6543	. . . . . . . . . . . . . . . 16 class ((𝑥(2nd ‘𝑓)𝑦)‘𝑘)
49	29, 34	cop 4600	. . . . . . . . . . . . . . . . 17 class ⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩
50	44, 33	cfv 6543	. . . . . . . . . . . . . . . . 17 class ((1st ‘𝑓)‘𝑦)
51	17	cv 1569	. . . . . . . . . . . . . . . . 17 class 𝑜
52	49, 50, 51	co 7423	. . . . . . . . . . . . . . . 16 class (⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))
53	48, 28, 52	co 7423	. . . . . . . . . . . . . . 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 7423	. . . . . . . . . . . . . 14 class (𝑥ℎ𝑦)
57	54, 41, 56	wreu 3370	. . . . . . . . . . . . 13 wff ∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
58	29, 50, 35	co 7423	. . . . . . . . . . . . 13 class (𝑤𝑗((1st ‘𝑓)‘𝑦))
59	57, 39, 58	wral 3082	. . . . . . . . . . . 12 wff ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
60	5	cv 1569	. . . . . . . . . . . 12 class 𝑏
61	59, 43, 60	wral 3082	. . . . . . . . . . 11 wff ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚)
62	38, 61	wa 401	. . . . . . . . . 10 wff ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))
63	62, 25, 27	copab 5178	. . . . . . . . 9 class {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))}
64	20, 21, 23, 24, 63	cmpo 7425	. . . . . . . 8 class (𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
65	17, 19, 64	csb 3856	. . . . . . 7 class ⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
66	15, 16, 65	csb 3856	. . . . . 6 class ⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
67	12, 14, 66	csb 3856	. . . . 5 class ⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
68	9, 11, 67	csb 3856	. . . 4 class ⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
69	5, 8, 68	csb 3856	. . 3 class ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})
70	2, 3, 4, 4, 69	cmpo 7425	. 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  49994  upfval  49995