Definition df-prstc 50132

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

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 50035), by prstcnid 50135, prstchom 50144, and prstcthin 50143. Other important properties include prstcbas 50136, prstcleval 50137, prstcle 50138, prstcocval 50139, prstcoc 50140, prstchom2 50145, and prstcprs 50142. Use those instead.

Note that the defining property prstchom 50144 is equivalent to prstchom2 50145 given prstcthin 50143. See thincn0eu 50013 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 50131	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18315	. . 3 class Proset
4	2	cv 1558	. . . . 5 class 𝑘
5		cnx 17220	. . . . . . 7 class ndx
6		chom 17288	. . . . . . 7 class Hom
7	5, 6	cfv 6516	. . . . . 6 class (Hom ‘ndx)
8		cple 17284	. . . . . . . 8 class le
9	4, 8	cfv 6516	. . . . . . 7 class (le‘𝑘)
10		c1o 8424	. . . . . . . 8 class 1o
11	10	csn 4579	. . . . . . 7 class {1o}
12	9, 11	cxp 5641	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4585	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17190	. . . . 5 class sSet
15	4, 13, 14	co 7391	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17289	. . . . . 6 class comp
17	5, 16	cfv 6516	. . . . 5 class (comp‘ndx)
18		c0 4283	. . . . 5 class ∅
19	17, 18	cop 4585	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7391	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5178	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1559	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  50133