Definition df-prstc 50627

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

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 50530), by prstcnid 50630, prstchom 50639, and prstcthin 50638. Other important properties include prstcbas 50631, prstcleval 50632, prstcle 50633, prstcocval 50634, prstcoc 50635, prstchom2 50640, and prstcprs 50637. Use those instead.

Note that the defining property prstchom 50639 is equivalent to prstchom2 50640 given prstcthin 50638. See thincn0eu 50508 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 50626	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18459	. . 3 class Proset
4	2	cv 1569	. . . . 5 class 𝑘
5		cnx 17364	. . . . . . 7 class ndx
6		chom 17432	. . . . . . 7 class Hom
7	5, 6	cfv 6537	. . . . . 6 class (Hom ‘ndx)
8		cple 17428	. . . . . . . 8 class le
9	4, 8	cfv 6537	. . . . . . 7 class (le‘𝑘)
10		c1o 8462	. . . . . . . 8 class 1o
11	10	csn 4584	. . . . . . 7 class {1o}
12	9, 11	cxp 5649	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4590	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17334	. . . . 5 class sSet
15	4, 13, 14	co 7418	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17433	. . . . . 6 class comp
17	5, 16	cfv 6537	. . . . 5 class (comp‘ndx)
18		c0 4279	. . . . 5 class ∅
19	17, 18	cop 4590	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7418	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5186	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1570	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is used by:  prstcval  50628