df-up

Given categories D and E , if F : D --> E is a functor and W an object of E , a universal pair from W to F is a pair <. X , M >. consisting of an object X of D and a morphism M : W --> F X of E , such that to every pair <. y , g >. with y an object of D and g : W --> F y a morphism of E , there is a unique morphism k : X --> y of D with F k .o. M = g . Such property is commonly referred to as a universal property. In our definition, it is denoted as X ( F ( D UP E ) W ) M .

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 M 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 <. X , M >. should be named differently as the morphism M , and thus we call X theuniversal object, M theuniversal morphism, and <. X , M >. theuniversal pair.

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

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

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-up

Detailed syntax breakdown