Metamath Proof Explorer

Theorem postc

Description: The converted category is a poset iff no distinct objects are isomorphic. (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses postc.c 
|- ( ph -> C = ( ProsetToCat ` K ) )
postc.k 
|- ( ph -> K e. Proset )
postc.b 
|- B = ( Base ` C )
Assertion postc 
|- ( ph -> ( C e. Poset <-> A. x e. B A. y e. B ( x ( ~=c ` C ) y -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 postc.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 postc.k 
 |-  ( ph -> K e. Proset )
3 postc.b 
 |-  B = ( Base ` C )
4 1 2 prstcprs 
 |-  ( ph -> C e. Proset )
5 eqid 
 |-  ( le ` C ) = ( le ` C )
6 3 5 ispos2 
 |-  ( C e. Poset <-> ( C e. Proset /\ A. x e. B A. y e. B ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
7 6 baib 
 |-  ( C e. Proset -> ( C e. Poset <-> A. x e. B A. y e. B ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
8 4 7 syl 
 |-  ( ph -> ( C e. Poset <-> A. x e. B A. y e. B ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
9 1 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> C = ( ProsetToCat ` K ) )
10 2 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> K e. Proset )
11 9 10 prstcthin 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. ThinCat )
12 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
13 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
14 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
15 11 3 12 13 14 thinccic 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( ~=c ` C ) y <-> ( ( x ( Hom ` C ) y ) =/= (/) /\ ( y ( Hom ` C ) x ) =/= (/) ) ) )
16 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( le ` C ) = ( le ` C ) )
17 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( Hom ` C ) = ( Hom ` C ) )
18 12 3 eleqtrdi 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. ( Base ` C ) )
19 13 3 eleqtrdi 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. ( Base ` C ) )
20 9 10 16 17 18 19 prstchom 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( le ` C ) y <-> ( x ( Hom ` C ) y ) =/= (/) ) )
21 9 10 16 17 19 18 prstchom 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y ( le ` C ) x <-> ( y ( Hom ` C ) x ) =/= (/) ) )
22 20 21 anbi12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x ( le ` C ) y /\ y ( le ` C ) x ) <-> ( ( x ( Hom ` C ) y ) =/= (/) /\ ( y ( Hom ` C ) x ) =/= (/) ) ) )
23 15 22 bitr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( ~=c ` C ) y <-> ( x ( le ` C ) y /\ y ( le ` C ) x ) ) )
24 23 imbi1d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x ( ~=c ` C ) y -> x = y ) <-> ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
25 24 2ralbidva 
 |-  ( ph -> ( A. x e. B A. y e. B ( x ( ~=c ` C ) y -> x = y ) <-> A. x e. B A. y e. B ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
26 8 25 bitr4d 
 |-  ( ph -> ( C e. Poset <-> A. x e. B A. y e. B ( x ( ~=c ` C ) y -> x = y ) ) )