Definition df-prstc 46232

Description: Definition of the function converting a preordered set to a category. Justified by prsthinc 46223.

This definition is somewhat arbitrary. Example 3.3(4.d) of [Adamek] p. 24 demonstrates an alternate definition with pairwise disjoint hom-sets. The behavior of the function is defined entirely, up to isomorphism, by prstcnid 46235, prstchom 46244, and prstcthin 46243. Other important properties include prstcbas 46236, prstcleval 46237, prstcle 46238, prstcocval 46239, prstcoc 46240, prstchom2 46245, and prstcprs 46242. Use those instead.

Note that the defining property prstchom 46244 is equivalent to prstchom2 46245 given prstcthin 46243. See thincn0eu 46201 for justification.

"ProsetToCat" was taken instead of "ProsetCat" because the latter might mean the category of preordered sets (classes). However, "ProsetToCat" seems too long. (Contributed by Zhi Wang, 20-Sep-2024.) (New usage is discouraged.)

Assertion

Ref	Expression
df-prstc	⊢ ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

Detailed syntax breakdown of Definition df-prstc

Step	Hyp	Ref	Expression
1		cprstc 46231	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 17926	. . 3 class Proset
4	2	cv 1538	. . . . 5 class 𝑘
5		cnx 16822	. . . . . . 7 class ndx
6		chom 16899	. . . . . . 7 class Hom
7	5, 6	cfv 6418	. . . . . 6 class (Hom ‘ndx)
8		cple 16895	. . . . . . . 8 class le
9	4, 8	cfv 6418	. . . . . . 7 class (le‘𝑘)
10		c1o 8260	. . . . . . . 8 class 1o
11	10	csn 4558	. . . . . . 7 class {1o}
12	9, 11	cxp 5578	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4564	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 16792	. . . . 5 class sSet
15	4, 13, 14	co 7255	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 16900	. . . . . 6 class comp
17	5, 16	cfv 6418	. . . . 5 class (comp‘ndx)
18		c0 4253	. . . . 5 class ∅
19	17, 18	cop 4564	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7255	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5153	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1539	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  46233