Definition df-prstc 50040

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

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 49943), by prstcnid 50043, prstchom 50052, and prstcthin 50051. Other important properties include prstcbas 50044, prstcleval 50045, prstcle 50046, prstcocval 50047, prstcoc 50048, prstchom2 50053, and prstcprs 50050. Use those instead.

Note that the defining property prstchom 50052 is equivalent to prstchom2 50053 given prstcthin 50051. See thincn0eu 49921 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 50039	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18249	. . 3 class Proset
4	2	cv 1546	. . . . 5 class 𝑘
5		cnx 17154	. . . . . . 7 class ndx
6		chom 17222	. . . . . . 7 class Hom
7	5, 6	cfv 6485	. . . . . 6 class (Hom ‘ndx)
8		cple 17218	. . . . . . . 8 class le
9	4, 8	cfv 6485	. . . . . . 7 class (le‘𝑘)
10		c1o 8388	. . . . . . . 8 class 1o
11	10	csn 4555	. . . . . . 7 class {1o}
12	9, 11	cxp 5616	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4561	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17124	. . . . 5 class sSet
15	4, 13, 14	co 7356	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17223	. . . . . 6 class comp
17	5, 16	cfv 6485	. . . . 5 class (comp‘ndx)
18		c0 4261	. . . . 5 class ∅
19	17, 18	cop 4561	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7356	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5153	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1547	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  50041