Definition df-prstc 51019

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

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 50919), by prstcnid 51022, prstchom 51031, and prstcthin 51030. Other important properties include prstcbas 51023, prstcleval 51024, prstcle 51025, prstcocval 51026, prstcoc 51027, prstchom2 51032, and prstcprs 51029. Use those instead.

Note that the defining property prstchom 51031 is equivalent to prstchom2 51032 given prstcthin 51030. See thincn0eu 50897 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 51018	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18516	. . 3 class Proset
4	2	cv 1569	. . . . 5 class 𝑘
5		cnx 17415	. . . . . . 7 class ndx
6		chom 17483	. . . . . . 7 class Hom
7	5, 6	cfv 6566	. . . . . 6 class (Hom ‘ndx)
8		cple 17479	. . . . . . . 8 class le
9	4, 8	cfv 6566	. . . . . . 7 class (le‘𝑘)
10		c1o 8507	. . . . . . . 8 class 1o
11	10	csn 4588	. . . . . . 7 class {1o}
12	9, 11	cxp 5656	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4840	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17385	. . . . 5 class sSet
15	4, 13, 14	co 7451	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17484	. . . . . 6 class comp
17	5, 16	cfv 6566	. . . . 5 class (comp‘ndx)
18		c0 4281	. . . . 5 class ∅
19	17, 18	cop 4840	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7451	. . 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 used by:  prstcval  51020