Definition df-prstc 50180

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

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 50083), by prstcnid 50183, prstchom 50192, and prstcthin 50191. Other important properties include prstcbas 50184, prstcleval 50185, prstcle 50186, prstcocval 50187, prstcoc 50188, prstchom2 50193, and prstcprs 50190. Use those instead.

Note that the defining property prstchom 50192 is equivalent to prstchom2 50193 given prstcthin 50191. See thincn0eu 50061 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 50179	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18336	. . 3 class Proset
4	2	cv 1562	. . . . 5 class 𝑘
5		cnx 17241	. . . . . . 7 class ndx
6		chom 17309	. . . . . . 7 class Hom
7	5, 6	cfv 6525	. . . . . 6 class (Hom ‘ndx)
8		cple 17305	. . . . . . . 8 class le
9	4, 8	cfv 6525	. . . . . . 7 class (le‘𝑘)
10		c1o 8434	. . . . . . . 8 class 1o
11	10	csn 4585	. . . . . . 7 class {1o}
12	9, 11	cxp 5649	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4591	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17211	. . . . 5 class sSet
15	4, 13, 14	co 7400	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17310	. . . . . 6 class comp
17	5, 16	cfv 6525	. . . . 5 class (comp‘ndx)
18		c0 4288	. . . . 5 class ∅
19	17, 18	cop 4591	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7400	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5185	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1563	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  50181