Definition df-prstc 50025

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

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 49928), by prstcnid 50028, prstchom 50037, and prstcthin 50036. Other important properties include prstcbas 50029, prstcleval 50030, prstcle 50031, prstcocval 50032, prstcoc 50033, prstchom2 50038, and prstcprs 50035. Use those instead.

Note that the defining property prstchom 50037 is equivalent to prstchom2 50038 given prstcthin 50036. See thincn0eu 49906 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 50024	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18258	. . 3 class Proset
4	2	cv 1541	. . . . 5 class 𝑘
5		cnx 17163	. . . . . . 7 class ndx
6		chom 17231	. . . . . . 7 class Hom
7	5, 6	cfv 6498	. . . . . 6 class (Hom ‘ndx)
8		cple 17227	. . . . . . . 8 class le
9	4, 8	cfv 6498	. . . . . . 7 class (le‘𝑘)
10		c1o 8398	. . . . . . . 8 class 1o
11	10	csn 4567	. . . . . . 7 class {1o}
12	9, 11	cxp 5629	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4573	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17133	. . . . 5 class sSet
15	4, 13, 14	co 7367	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17232	. . . . . 6 class comp
17	5, 16	cfv 6498	. . . . 5 class (comp‘ndx)
18		c0 4273	. . . . 5 class ∅
19	17, 18	cop 4573	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7367	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5166	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1542	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  50026