Definition df-prstc 49539

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

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 49442), by prstcnid 49542, prstchom 49551, and prstcthin 49550. Other important properties include prstcbas 49543, prstcleval 49544, prstcle 49545, prstcocval 49546, prstcoc 49547, prstchom2 49552, and prstcprs 49549. Use those instead.

Note that the defining property prstchom 49551 is equivalent to prstchom2 49552 given prstcthin 49550. See thincn0eu 49420 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 49538	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18253	. . 3 class Proset
4	2	cv 1539	. . . . 5 class 𝑘
5		cnx 17163	. . . . . . 7 class ndx
6		chom 17231	. . . . . . 7 class Hom
7	5, 6	cfv 6511	. . . . . 6 class (Hom ‘ndx)
8		cple 17227	. . . . . . . 8 class le
9	4, 8	cfv 6511	. . . . . . 7 class (le‘𝑘)
10		c1o 8427	. . . . . . . 8 class 1o
11	10	csn 4589	. . . . . . 7 class {1o}
12	9, 11	cxp 5636	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4595	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17133	. . . . 5 class sSet
15	4, 13, 14	co 7387	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17232	. . . . . 6 class comp
17	5, 16	cfv 6511	. . . . 5 class (comp‘ndx)
18		c0 4296	. . . . 5 class ∅
19	17, 18	cop 4595	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7387	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5188	. 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  49540