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

Metamath Proof Explorer

Theorem prstcprs

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

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

Proof

Step Hyp Ref Expression
1 prstcnid.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 prstcnid.k 
 |-  ( ph -> K e. Proset )
3 eqidd 
 |-  ( ph -> ( Base ` K ) = ( Base ` K ) )
4 1 2 3 prstcbas 
 |-  ( ph -> ( Base ` K ) = ( Base ` C ) )
5 eqidd 
 |-  ( ph -> ( le ` K ) = ( le ` K ) )
6 1 2 5 prstcleval 
 |-  ( ph -> ( le ` K ) = ( le ` C ) )
7 fvex 
 |-  ( ProsetToCat ` K ) e. _V
8 1 7 eqeltrdi 
 |-  ( ph -> C e. _V )
9 4 6 8 isprsd 
 |-  ( ph -> ( C e. Proset <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
10 3 5 2 isprsd 
 |-  ( ph -> ( K e. Proset <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
11 9 10 bitr4d 
 |-  ( ph -> ( C e. Proset <-> K e. Proset ) )
12 2 11 mpbird 
 |-  ( ph -> C e. Proset )