Metamath Proof Explorer

Theorem posprs

Description: A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion posprs 
|- ( K e. Poset -> K e. Proset )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` K ) = ( Base ` K )
2 eqid 
 |-  ( le ` K ) = ( le ` K )
3 1 2 ispos2 
 |-  ( K e. Poset <-> ( K e. Proset /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) ) )
4 3 simplbi 
 |-  ( K e. Poset -> K e. Proset )