Definition df-prstc 50208

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

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 (thincciso 50111), by prstcnid 50211, prstchom 50220, and prstcthin 50219. Other important properties include prstcbas 50212, prstcleval 50213, prstcle 50214, prstcocval 50215, prstcoc 50216, prstchom2 50221, and prstcprs 50218. Use those instead.

Note that the defining property prstchom 50220 is equivalent to prstchom2 50221 given prstcthin 50219. See thincn0eu 50089 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 50207	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18344	. . 3 class Proset
4	2	cv 1566	. . . . 5 class 𝑘
5		cnx 17249	. . . . . . 7 class ndx
6		chom 17317	. . . . . . 7 class Hom
7	5, 6	cfv 6534	. . . . . 6 class (Hom ‘ndx)
8		cple 17313	. . . . . . . 8 class le
9	4, 8	cfv 6534	. . . . . . 7 class (le‘𝑘)
10		c1o 8442	. . . . . . . 8 class 1o
11	10	csn 4591	. . . . . . 7 class {1o}
12	9, 11	cxp 5657	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4597	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17219	. . . . 5 class sSet
15	4, 13, 14	co 7408	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17318	. . . . . 6 class comp
17	5, 16	cfv 6534	. . . . 5 class (comp‘ndx)
18		c0 4294	. . . . 5 class ∅
19	17, 18	cop 4597	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7408	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5193	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1567	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  50209