Metamath Proof Explorer

Theorem prstcthin

Description: The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024)

Ref Expression
Hypotheses prstcnid.c 
|- ( ph -> C = ( ProsetToCat ` K ) )
prstcnid.k 
|- ( ph -> K e. Proset )
Assertion prstcthin 
|- ( ph -> C e. ThinCat )

Proof

Step Hyp Ref Expression
1 prstcnid.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 prstcnid.k 
 |-  ( ph -> K e. Proset )
3 eqidd 
 |-  ( ph -> ( Base ` C ) = ( Base ` C ) )
4 eqidd 
 |-  ( ph -> ( le ` C ) = ( le ` C ) )
5 1 2 4 prstchomval 
 |-  ( ph -> ( ( le ` C ) X. { 1o } ) = ( Hom ` C ) )
6 ovex 
 |-  ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) e. _V
7 0ex 
 |-  (/) e. _V
8 ccoid 
 |-  comp = Slot ( comp ` ndx )
9 8 setsid 
 |-  ( ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) e. _V /\ (/) e. _V ) -> (/) = ( comp ` ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) )
10 6 7 9 mp2an 
 |-  (/) = ( comp ` ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )
11 1 2 prstcval 
 |-  ( ph -> C = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )
12 11 fveq2d 
 |-  ( ph -> ( comp ` C ) = ( comp ` ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) )
13 10 12 eqtr4id 
 |-  ( ph -> (/) = ( comp ` C ) )
14 1 2 prstcprs 
 |-  ( ph -> C e. Proset )
15 3 5 13 4 14 prsthinc 
 |-  ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. ( Base ` C ) |-> (/) ) ) )
16 15 simpld 
 |-  ( ph -> C e. ThinCat )