Definition df-prstc 50037

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

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 49940), by prstcnid 50040, prstchom 50049, and prstcthin 50048. Other important properties include prstcbas 50041, prstcleval 50042, prstcle 50043, prstcocval 50044, prstcoc 50045, prstchom2 50050, and prstcprs 50047. Use those instead.

Note that the defining property prstchom 50049 is equivalent to prstchom2 50050 given prstcthin 50048. See thincn0eu 49918 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 50036	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18249	. . 3 class Proset
4	2	cv 1541	. . . . 5 class 𝑘
5		cnx 17154	. . . . . . 7 class ndx
6		chom 17222	. . . . . . 7 class Hom
7	5, 6	cfv 6492	. . . . . 6 class (Hom ‘ndx)
8		cple 17218	. . . . . . . 8 class le
9	4, 8	cfv 6492	. . . . . . 7 class (le‘𝑘)
10		c1o 8391	. . . . . . . 8 class 1o
11	10	csn 4568	. . . . . . 7 class {1o}
12	9, 11	cxp 5622	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4574	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17124	. . . . 5 class sSet
15	4, 13, 14	co 7360	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17223	. . . . . 6 class comp
17	5, 16	cfv 6492	. . . . 5 class (comp‘ndx)
18		c0 4274	. . . . 5 class ∅
19	17, 18	cop 4574	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7360	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5167	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1542	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is referenced by:  prstcval  50038