Description: Preordered sets as categories. Similar to example 3.3(4.d) of Adamek p. 24, but the hom-sets are not pairwise disjoint. One can define a functor from the category of prosets to the category of small thin categories. See catprs and catprs2 for inducing a preorder from a category. Example 3.26(2) of Adamek p. 33 indicates that it induces a bijection from the equivalence class of isomorphic small thin categories to the equivalence class of order-isomorphic preordered sets. (Contributed by Zhi Wang, 18-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | indthinc.b | |
|
prsthinc.h | |
||
prsthinc.o | |
||
prsthinc.l | |
||
prsthinc.p | |
||
Assertion | prsthinc | Could not format assertion : No typesetting found for |- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) ) with typecode |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | indthinc.b | |
|
2 | prsthinc.h | |
|
3 | prsthinc.o | |
|
4 | prsthinc.l | |
|
5 | prsthinc.p | |
|
6 | eqidd | |
|
7 | 6 | f1omo | |
8 | df-ov | |
|
9 | 8 | eleq2i | |
10 | 9 | mobii | |
11 | 7 10 | sylibr | |
12 | biid | |
|
13 | 0lt1o | |
|
14 | 1 | eleq2d | |
15 | eqid | |
|
16 | eqid | |
|
17 | 15 16 | prsref | |
18 | 5 17 | sylan | |
19 | 14 18 | sylbida | |
20 | 4 | breqd | |
21 | 20 | biimpar | |
22 | 19 21 | syldan | |
23 | eqidd | |
|
24 | 1oex | |
|
25 | 24 | a1i | |
26 | 1n0 | |
|
27 | 26 | a1i | |
28 | 23 25 27 | fvconstr | |
29 | 22 28 | mpbid | |
30 | 13 29 | eleqtrrid | |
31 | 0ov | |
|
32 | 31 | oveqi | |
33 | 0ov | |
|
34 | 32 33 | eqtri | |
35 | 34 13 | eqeltri | |
36 | simpl | |
|
37 | 5 | adantr | |
38 | 1 | eleq2d | |
39 | 1 | eleq2d | |
40 | 38 14 39 | 3anbi123d | |
41 | 40 | biimpa | |
42 | 41 | adantrr | |
43 | eqidd | |
|
44 | simprrl | |
|
45 | 43 44 | fvconstr2 | |
46 | 4 | breqd | |
47 | 46 | biimpd | |
48 | 36 45 47 | sylc | |
49 | simprrr | |
|
50 | 43 49 | fvconstr2 | |
51 | 4 | breqd | |
52 | 51 | biimpd | |
53 | 36 50 52 | sylc | |
54 | 15 16 | prstr | |
55 | 37 42 48 53 54 | syl112anc | |
56 | 4 | breqd | |
57 | 56 | biimprd | |
58 | 36 55 57 | sylc | |
59 | 24 | a1i | |
60 | 26 | a1i | |
61 | 43 59 60 | fvconstr | |
62 | 58 61 | mpbid | |
63 | 35 62 | eleqtrrid | |
64 | 1 2 11 3 5 12 30 63 | isthincd2 | Could not format ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) ) : No typesetting found for |- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) ) with typecode |- |