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 
|- ( ph -> B = ( Base ` C ) )
prsthinc.h 
|- ( ph -> ( .<_ X. { 1o } ) = ( Hom ` C ) )
prsthinc.o 
|- ( ph -> (/) = ( comp ` C ) )
prsthinc.l 
|- ( ph -> .<_ = ( le ` C ) )
prsthinc.p 
|- ( ph -> C e. Proset )
Assertion prsthinc 
|- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) )

Proof

Step Hyp Ref Expression
1 indthinc.b 
 |-  ( ph -> B = ( Base ` C ) )
2 prsthinc.h 
 |-  ( ph -> ( .<_ X. { 1o } ) = ( Hom ` C ) )
3 prsthinc.o 
 |-  ( ph -> (/) = ( comp ` C ) )
4 prsthinc.l 
 |-  ( ph -> .<_ = ( le ` C ) )
5 prsthinc.p 
 |-  ( ph -> C e. Proset )
6 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( .<_ X. { 1o } ) = ( .<_ X. { 1o } ) )
7 6 f1omo 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( ( .<_ X. { 1o } ) ` <. x , y >. ) )
8 df-ov 
 |-  ( x ( .<_ X. { 1o } ) y ) = ( ( .<_ X. { 1o } ) ` <. x , y >. )
9 8 eleq2i 
 |-  ( f e. ( x ( .<_ X. { 1o } ) y ) <-> f e. ( ( .<_ X. { 1o } ) ` <. x , y >. ) )
10 9 mobii 
 |-  ( E* f f e. ( x ( .<_ X. { 1o } ) y ) <-> E* f f e. ( ( .<_ X. { 1o } ) ` <. x , y >. ) )
11 7 10 sylibr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x ( .<_ X. { 1o } ) y ) )
12 biid 
 |-  ( ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) <-> ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) )
13 0lt1o 
 |-  (/) e. 1o
14 1 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( Base ` C ) ) )
15 eqid 
 |-  ( Base ` C ) = ( Base ` C )
16 eqid 
 |-  ( le ` C ) = ( le ` C )
17 15 16 prsref 
 |-  ( ( C e. Proset /\ y e. ( Base ` C ) ) -> y ( le ` C ) y )
18 5 17 sylan 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> y ( le ` C ) y )
19 14 18 sylbida 
 |-  ( ( ph /\ y e. B ) -> y ( le ` C ) y )
20 4 breqd 
 |-  ( ph -> ( y .<_ y <-> y ( le ` C ) y ) )
21 20 biimpar 
 |-  ( ( ph /\ y ( le ` C ) y ) -> y .<_ y )
22 19 21 syldan 
 |-  ( ( ph /\ y e. B ) -> y .<_ y )
23 eqidd 
 |-  ( ( ph /\ y e. B ) -> ( .<_ X. { 1o } ) = ( .<_ X. { 1o } ) )
24 1oex 
 |-  1o e. _V
25 24 a1i 
 |-  ( ( ph /\ y e. B ) -> 1o e. _V )
26 1n0 
 |-  1o =/= (/)
27 26 a1i 
 |-  ( ( ph /\ y e. B ) -> 1o =/= (/) )
28 23 25 27 fvconstr 
 |-  ( ( ph /\ y e. B ) -> ( y .<_ y <-> ( y ( .<_ X. { 1o } ) y ) = 1o ) )
29 22 28 mpbid 
 |-  ( ( ph /\ y e. B ) -> ( y ( .<_ X. { 1o } ) y ) = 1o )
30 13 29 eleqtrrid 
 |-  ( ( ph /\ y e. B ) -> (/) e. ( y ( .<_ X. { 1o } ) y ) )
31 0ov 
 |-  ( <. x , y >. (/) z ) = (/)
32 31 oveqi 
 |-  ( g ( <. x , y >. (/) z ) f ) = ( g (/) f )
33 0ov 
 |-  ( g (/) f ) = (/)
34 32 33 eqtri 
 |-  ( g ( <. x , y >. (/) z ) f ) = (/)
35 34 13 eqeltri 
 |-  ( g ( <. x , y >. (/) z ) f ) e. 1o
36 simpl 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> ph )
37 5 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> C e. Proset )
38 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` C ) ) )
39 1 eleq2d 
 |-  ( ph -> ( z e. B <-> z e. ( Base ` C ) ) )
40 38 14 39 3anbi123d 
 |-  ( ph -> ( ( x e. B /\ y e. B /\ z e. B ) <-> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) )
41 40 biimpa 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) )
42 41 adantrr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) )
43 eqidd 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> ( .<_ X. { 1o } ) = ( .<_ X. { 1o } ) )
44 simprrl 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> f e. ( x ( .<_ X. { 1o } ) y ) )
45 43 44 fvconstr2 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> x .<_ y )
46 4 breqd 
 |-  ( ph -> ( x .<_ y <-> x ( le ` C ) y ) )
47 46 biimpd 
 |-  ( ph -> ( x .<_ y -> x ( le ` C ) y ) )
48 36 45 47 sylc 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> x ( le ` C ) y )
49 simprrr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> g e. ( y ( .<_ X. { 1o } ) z ) )
50 43 49 fvconstr2 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> y .<_ z )
51 4 breqd 
 |-  ( ph -> ( y .<_ z <-> y ( le ` C ) z ) )
52 51 biimpd 
 |-  ( ph -> ( y .<_ z -> y ( le ` C ) z ) )
53 36 50 52 sylc 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> y ( le ` C ) z )
54 15 16 prstr 
 |-  ( ( C e. Proset /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( x ( le ` C ) y /\ y ( le ` C ) z ) ) -> x ( le ` C ) z )
55 37 42 48 53 54 syl112anc 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> x ( le ` C ) z )
56 4 breqd 
 |-  ( ph -> ( x .<_ z <-> x ( le ` C ) z ) )
57 56 biimprd 
 |-  ( ph -> ( x ( le ` C ) z -> x .<_ z ) )
58 36 55 57 sylc 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> x .<_ z )
59 24 a1i 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> 1o e. _V )
60 26 a1i 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> 1o =/= (/) )
61 43 59 60 fvconstr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> ( x .<_ z <-> ( x ( .<_ X. { 1o } ) z ) = 1o ) )
62 58 61 mpbid 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> ( x ( .<_ X. { 1o } ) z ) = 1o )
63 35 62 eleqtrrid 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( .<_ X. { 1o } ) y ) /\ g e. ( y ( .<_ X. { 1o } ) z ) ) ) ) -> ( g ( <. x , y >. (/) z ) f ) e. ( x ( .<_ X. { 1o } ) z ) )
64 1 2 11 3 5 12 30 63 isthincd2 
 |-  ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) )