Metamath Proof Explorer


Theorem prsthinc

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 φB=BaseC
prsthinc.h φ˙×1𝑜=HomC
prsthinc.o φ=compC
prsthinc.l φ˙=C
prsthinc.p φCProset
Assertion prsthinc Could not format assertion : No typesetting found for |- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 indthinc.b φB=BaseC
2 prsthinc.h φ˙×1𝑜=HomC
3 prsthinc.o φ=compC
4 prsthinc.l φ˙=C
5 prsthinc.p φCProset
6 eqidd φxByB˙×1𝑜=˙×1𝑜
7 6 f1omo φxByB*ff˙×1𝑜xy
8 df-ov x˙×1𝑜y=˙×1𝑜xy
9 8 eleq2i fx˙×1𝑜yf˙×1𝑜xy
10 9 mobii *ffx˙×1𝑜y*ff˙×1𝑜xy
11 7 10 sylibr φxByB*ffx˙×1𝑜y
12 biid xByBzBfx˙×1𝑜ygy˙×1𝑜zxByBzBfx˙×1𝑜ygy˙×1𝑜z
13 0lt1o 1𝑜
14 1 eleq2d φyByBaseC
15 eqid BaseC=BaseC
16 eqid C=C
17 15 16 prsref CProsetyBaseCyCy
18 5 17 sylan φyBaseCyCy
19 14 18 sylbida φyByCy
20 4 breqd φy˙yyCy
21 20 biimpar φyCyy˙y
22 19 21 syldan φyBy˙y
23 eqidd φyB˙×1𝑜=˙×1𝑜
24 1oex 1𝑜V
25 24 a1i φyB1𝑜V
26 1n0 1𝑜
27 26 a1i φyB1𝑜
28 23 25 27 fvconstr φyBy˙yy˙×1𝑜y=1𝑜
29 22 28 mpbid φyBy˙×1𝑜y=1𝑜
30 13 29 eleqtrrid φyBy˙×1𝑜y
31 0ov xyz=
32 31 oveqi gxyzf=gf
33 0ov gf=
34 32 33 eqtri gxyzf=
35 34 13 eqeltri gxyzf1𝑜
36 simpl φxByBzBfx˙×1𝑜ygy˙×1𝑜zφ
37 5 adantr φxByBzBfx˙×1𝑜ygy˙×1𝑜zCProset
38 1 eleq2d φxBxBaseC
39 1 eleq2d φzBzBaseC
40 38 14 39 3anbi123d φxByBzBxBaseCyBaseCzBaseC
41 40 biimpa φxByBzBxBaseCyBaseCzBaseC
42 41 adantrr φxByBzBfx˙×1𝑜ygy˙×1𝑜zxBaseCyBaseCzBaseC
43 eqidd φxByBzBfx˙×1𝑜ygy˙×1𝑜z˙×1𝑜=˙×1𝑜
44 simprrl φxByBzBfx˙×1𝑜ygy˙×1𝑜zfx˙×1𝑜y
45 43 44 fvconstr2 φxByBzBfx˙×1𝑜ygy˙×1𝑜zx˙y
46 4 breqd φx˙yxCy
47 46 biimpd φx˙yxCy
48 36 45 47 sylc φxByBzBfx˙×1𝑜ygy˙×1𝑜zxCy
49 simprrr φxByBzBfx˙×1𝑜ygy˙×1𝑜zgy˙×1𝑜z
50 43 49 fvconstr2 φxByBzBfx˙×1𝑜ygy˙×1𝑜zy˙z
51 4 breqd φy˙zyCz
52 51 biimpd φy˙zyCz
53 36 50 52 sylc φxByBzBfx˙×1𝑜ygy˙×1𝑜zyCz
54 15 16 prstr CProsetxBaseCyBaseCzBaseCxCyyCzxCz
55 37 42 48 53 54 syl112anc φxByBzBfx˙×1𝑜ygy˙×1𝑜zxCz
56 4 breqd φx˙zxCz
57 56 biimprd φxCzx˙z
58 36 55 57 sylc φxByBzBfx˙×1𝑜ygy˙×1𝑜zx˙z
59 24 a1i φxByBzBfx˙×1𝑜ygy˙×1𝑜z1𝑜V
60 26 a1i φxByBzBfx˙×1𝑜ygy˙×1𝑜z1𝑜
61 43 59 60 fvconstr φxByBzBfx˙×1𝑜ygy˙×1𝑜zx˙zx˙×1𝑜z=1𝑜
62 58 61 mpbid φxByBzBfx˙×1𝑜ygy˙×1𝑜zx˙×1𝑜z=1𝑜
63 35 62 eleqtrrid φxByBzBfx˙×1𝑜ygy˙×1𝑜zgxyzfx˙×1𝑜z
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 |-