Definition df-prstc 49375

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

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 49287), by prstcnid 49378, prstchom 49387, and prstcthin 49386. Other important properties include prstcbas 49379, prstcleval 49380, prstcle 49381, prstcocval 49382, prstcoc 49383, prstchom2 49388, and prstcprs 49385. Use those instead.

Note that the defining property prstchom 49387 is equivalent to prstchom2 49388 given prstcthin 49386. See thincn0eu 49265 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 49374	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18302	. . 3 class Proset
4	2	cv 1539	. . . . 5 class 𝑘
5		cnx 17210	. . . . . . 7 class ndx
6		chom 17280	. . . . . . 7 class Hom
7	5, 6	cfv 6530	. . . . . 6 class (Hom ‘ndx)
8		cple 17276	. . . . . . . 8 class le
9	4, 8	cfv 6530	. . . . . . 7 class (le‘𝑘)
10		c1o 8471	. . . . . . . 8 class 1o
11	10	csn 4601	. . . . . . 7 class {1o}
12	9, 11	cxp 5652	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4607	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17180	. . . . 5 class sSet
15	4, 13, 14	co 7403	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17281	. . . . . 6 class comp
17	5, 16	cfv 6530	. . . . 5 class (comp‘ndx)
18		c0 4308	. . . . 5 class ∅
19	17, 18	cop 4607	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7403	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5201	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1540	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  49376