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 18216	. . 3 class Proset
4	2	cv 1539	. . . . 5 class 𝑘
5		cnx 17122	. . . . . . 7 class ndx
6		chom 17190	. . . . . . 7 class Hom
7	5, 6	cfv 6486	. . . . . 6 class (Hom ‘ndx)
8		cple 17186	. . . . . . . 8 class le
9	4, 8	cfv 6486	. . . . . . 7 class (le‘𝑘)
10		c1o 8388	. . . . . . . 8 class 1o
11	10	csn 4579	. . . . . . 7 class {1o}
12	9, 11	cxp 5621	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4585	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17092	. . . . 5 class sSet
15	4, 13, 14	co 7353	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17191	. . . . . 6 class comp
17	5, 16	cfv 6486	. . . . 5 class (comp‘ndx)
18		c0 4286	. . . . 5 class ∅
19	17, 18	cop 4585	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7353	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5176	. 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