Definition df-prstc 49543

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

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 49446), by prstcnid 49546, prstchom 49555, and prstcthin 49554. Other important properties include prstcbas 49547, prstcleval 49548, prstcle 49549, prstcocval 49550, prstcoc 49551, prstchom2 49556, and prstcprs 49553. Use those instead.

Note that the defining property prstchom 49555 is equivalent to prstchom2 49556 given prstcthin 49554. See thincn0eu 49424 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 49542	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18260	. . 3 class Proset
4	2	cv 1539	. . . . 5 class 𝑘
5		cnx 17170	. . . . . . 7 class ndx
6		chom 17238	. . . . . . 7 class Hom
7	5, 6	cfv 6514	. . . . . 6 class (Hom ‘ndx)
8		cple 17234	. . . . . . . 8 class le
9	4, 8	cfv 6514	. . . . . . 7 class (le‘𝑘)
10		c1o 8430	. . . . . . . 8 class 1o
11	10	csn 4592	. . . . . . 7 class {1o}
12	9, 11	cxp 5639	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4598	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17140	. . . . 5 class sSet
15	4, 13, 14	co 7390	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17239	. . . . . 6 class comp
17	5, 16	cfv 6514	. . . . 5 class (comp‘ndx)
18		c0 4299	. . . . 5 class ∅
19	17, 18	cop 4598	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7390	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5191	. 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  49544