Definition df-prstc 50796

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

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 50696), by prstcnid 50799, prstchom 50808, and prstcthin 50807. Other important properties include prstcbas 50800, prstcleval 50801, prstcle 50802, prstcocval 50803, prstcoc 50804, prstchom2 50809, and prstcprs 50806. Use those instead.

Note that the defining property prstchom 50808 is equivalent to prstchom2 50809 given prstcthin 50807. See thincn0eu 50674 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 50795	. 2 class ProsetToCat
2		vk	. . 3 setvar 𝑘
3		cproset 18475	. . 3 class Proset
4	2	cv 1568	. . . . 5 class 𝑘
5		cnx 17380	. . . . . . 7 class ndx
6		chom 17448	. . . . . . 7 class Hom
7	5, 6	cfv 6543	. . . . . 6 class (Hom ‘ndx)
8		cple 17444	. . . . . . . 8 class le
9	4, 8	cfv 6543	. . . . . . 7 class (le‘𝑘)
10		c1o 8476	. . . . . . . 8 class 1o
11	10	csn 4584	. . . . . . 7 class {1o}
12	9, 11	cxp 5649	. . . . . 6 class ((le‘𝑘) × {1o})
13	7, 12	cop 4834	. . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14		csts 17350	. . . . 5 class sSet
15	4, 13, 14	co 7424	. . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16		cco 17449	. . . . . 6 class comp
17	5, 16	cfv 6543	. . . . 5 class (comp‘ndx)
18		c0 4277	. . . . 5 class ∅
19	17, 18	cop 4834	. . . 4 class ⟨(comp‘ndx), ∅⟩
20	15, 19, 14	co 7424	. . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
21	2, 3, 20	cmpt 5185	. 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
22	1, 21	wceq 1569	1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))

This definition is used by:  prstcval  50797