Definition df-prstc 50328

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

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 50231), by prstcnid 50331, prstchom 50340, and prstcthin 50339. Other important properties include prstcbas 50332, prstcleval 50333, prstcle 50334, prstcocval 50335, prstcoc 50336, prstchom2 50341, and prstcprs 50338. Use those instead.

Note that the defining property prstchom 50340 is equivalent to prstchom2 50341 given prstcthin 50339. See thincn0eu 50209 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 50327	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18343	. . 3 class Proset
4	2	cv 1569	. . . . 5 class 𝑘
5		cnx 17248	. . . . . . 7 class ndx
6		chom 17316	. . . . . . 7 class Hom
7	5, 6	cfv 6536	. . . . . 6 class (Hom ‘ndx)
8		cple 17312	. . . . . . . 8 class le
9	4, 8	cfv 6536	. . . . . . 7 class (le‘𝑘)
10		c1o 8442	. . . . . . . 8 class 1o
11	10	csn 4589	. . . . . . 7 class {1o}
12	9, 11	cxp 5659	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4595	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17218	. . . . 5 class sSet
15	4, 13, 14	co 7410	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17317	. . . . . 6 class comp
17	5, 16	cfv 6536	. . . . 5 class (comp‘ndx)
18		c0 4286	. . . . 5 class ∅
19	17, 18	cop 4595	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7410	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5192	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1570	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  50329