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 47173
Description: Definition of the function converting a preordered set to a category. Justified by prsthinc 47164.

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 47176, prstchom 47187, and prstcthin 47186. Other important properties include prstcbas 47177, prstcleval 47178, prstcle 47180, prstcocval 47181, prstcoc 47183, prstchom2 47188, and prstcprs 47185. Use those instead.

Note that the defining property prstchom 47187 is equivalent to prstchom2 47188 given prstcthin 47186. See thincn0eu 47142 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 47172 . 2 class ProsetToCat
2 vk . . 3 setvar 𝑘
3 cproset 18190 . . 3 class Proset
42cv 1541 . . . . 5 class 𝑘
5 cnx 17073 . . . . . . 7 class ndx
6 chom 17152 . . . . . . 7 class Hom
75, 6cfv 6500 . . . . . 6 class (Hom ‘ndx)
8 cple 17148 . . . . . . . 8 class le
94, 8cfv 6500 . . . . . . 7 class (le‘𝑘)
10 c1o 8409 . . . . . . . 8 class 1o
1110csn 4590 . . . . . . 7 class {1o}
129, 11cxp 5635 . . . . . 6 class ((le‘𝑘) × {1o})
137, 12cop 4596 . . . . 5 class ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩
14 csts 17043 . . . . 5 class sSet
154, 13, 14co 7361 . . . 4 class (𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩)
16 cco 17153 . . . . . 6 class comp
175, 16cfv 6500 . . . . 5 class (comp‘ndx)
18 c0 4286 . . . . 5 class
1917, 18cop 4596 . . . 4 class ⟨(comp‘ndx), ∅⟩
2015, 19, 14co 7361 . . 3 class ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩)
212, 3, 20cmpt 5192 . 2 class (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
221, 21wceq 1542 1 wff ProsetToCat = (𝑘 ∈ Proset ↦ ((𝑘 sSet ⟨(Hom ‘ndx), ((le‘𝑘) × {1o})⟩) sSet ⟨(comp‘ndx), ∅⟩))
Colors of variables: wff setvar class
This definition is referenced by:  prstcval  47174
  Copyright terms: Public domain W3C validator