Definition df-prstc 50476

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

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 50379), by prstcnid 50479, prstchom 50488, and prstcthin 50487. Other important properties include prstcbas 50480, prstcleval 50481, prstcle 50482, prstcocval 50483, prstcoc 50484, prstchom2 50489, and prstcprs 50486. Use those instead.

Note that the defining property prstchom 50488 is equivalent to prstchom2 50489 given prstcthin 50487. See thincn0eu 50357 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 50475	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18380	. . 3 class Proset
4	2	cv 1569	. . . . 5 class 𝑘
5		cnx 17285	. . . . . . 7 class ndx
6		chom 17353	. . . . . . 7 class Hom
7	5, 6	cfv 6533	. . . . . 6 class (Hom ‘ndx)
8		cple 17349	. . . . . . . 8 class le
9	4, 8	cfv 6533	. . . . . . 7 class (le‘𝑘)
10		c1o 8448	. . . . . . . 8 class 1o
11	10	csn 4584	. . . . . . 7 class {1o}
12	9, 11	cxp 5653	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4590	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17255	. . . . 5 class sSet
15	4, 13, 14	co 7413	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17354	. . . . . 6 class comp
17	5, 16	cfv 6533	. . . . 5 class (comp‘ndx)
18		c0 4279	. . . . 5 class ∅
19	17, 18	cop 4590	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7413	. . 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  50477