Definition df-prstc 48730

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

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 48733, prstchom 48744, and prstcthin 48743. Other important properties include prstcbas 48734, prstcleval 48735, prstcle 48737, prstcocval 48738, prstcoc 48740, prstchom2 48745, and prstcprs 48742. Use those instead.

Note that the defining property prstchom 48744 is equivalent to prstchom2 48745 given prstcthin 48743. See thincn0eu 48699 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 48729	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18363	. . 3 class Proset
4	2	cv 1536	. . . . 5 class 𝑘
5		cnx 17240	. . . . . . 7 class ndx
6		chom 17322	. . . . . . 7 class Hom
7	5, 6	cfv 6573	. . . . . 6 class (Hom ‘ndx)
8		cple 17318	. . . . . . . 8 class le
9	4, 8	cfv 6573	. . . . . . 7 class (le‘𝑘)
10		c1o 8515	. . . . . . . 8 class 1o
11	10	csn 4648	. . . . . . 7 class {1o}
12	9, 11	cxp 5698	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4654	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17210	. . . . 5 class sSet
15	4, 13, 14	co 7448	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17323	. . . . . 6 class comp
17	5, 16	cfv 6573	. . . . 5 class (comp‘ndx)
18		c0 4352	. . . . 5 class ∅
19	17, 18	cop 4654	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7448	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5249	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1537	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  48731