This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem postcpos

Description: The converted category is a poset iff the original proset is a poset. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses postc.c 
|- ( ph -> C = ( ProsetToCat ` K ) )
postc.k 
|- ( ph -> K e. Proset )
Assertion postcpos 
|- ( ph -> ( K e. Poset <-> C e. Poset ) )

Proof

Step Hyp Ref Expression
1 postc.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 postc.k 
 |-  ( ph -> K e. Proset )
3 1 2 prstcprs 
 |-  ( ph -> C e. Proset )
4 eqidd 
 |-  ( ph -> ( Base ` K ) = ( Base ` K ) )
5 1 2 4 prstcbas 
 |-  ( ph -> ( Base ` K ) = ( Base ` C ) )
6 eqidd 
 |-  ( ph -> ( le ` K ) = ( le ` K ) )
7 1 2 6 prstcle 
 |-  ( ph -> ( x ( le ` K ) y <-> x ( le ` C ) y ) )
8 7 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( le ` K ) y <-> x ( le ` C ) y ) )
9 2 3 4 5 8 pospropd 
 |-  ( ph -> ( K e. Poset <-> C e. Poset ) )