Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prstc Structured version   Visualization version   GIF version

Definition df-prstc 46344
Description: Definition of the function converting a preordered set to a category. Justified by prsthinc 46335.

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, by prstcnid 46347, prstchom 46358, and prstcthin 46357. Other important properties include prstcbas 46348, prstcleval 46349, prstcle 46351, prstcocval 46352, prstcoc 46354, prstchom2 46359, and prstcprs 46356. Use those instead.

Note that the defining property prstchom 46358 is equivalent to prstchom2 46359 given prstcthin 46357. See thincn0eu 46313 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
StepHypRef Expression
1 cprstc 46343 . 2 class ProsetToCat
2 vk . . 3 setvar 𝑘
3 cproset 18011 . . 3 class Proset
42cv 1538 . . . . 5 class 𝑘
5 cnx 16894 . . . . . . 7 class ndx
6 chom 16973 . . . . . . 7 class Hom
75, 6cfv 6433 . . . . . 6 class (Hom ‘ndx)
8 cple 16969 . . . . . . . 8 class le
94, 8cfv 6433 . . . . . . 7 class (le‘𝑘)
10 c1o 8290 . . . . . . . 8 class 1o
1110csn 4561 . . . . . . 7 class {1o}
129, 11cxp 5587 . . . . . 6 class ((le‘𝑘) × {1o})
137, 12cop 4567 . . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14 csts 16864 . . . . 5 class sSet
154, 13, 14co 7275 . . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16 cco 16974 . . . . . 6 class comp
175, 16cfv 6433 . . . . 5 class (comp‘ndx)
18 c0 4256 . . . . 5 class
1917, 18cop 4567 . . . 4 class ⟨(comp‘ndx), ∅⟩
2015, 19, 14co 7275 . . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
212, 3, 20cmpt 5157 . 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
221, 21wceq 1539 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Colors of variables: wff setvar class
This definition is referenced by:  prstcval  46345
  Copyright terms: Public domain W3C validator