Metamath Proof Explorer

Theorem tospos

Description: A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018)

Ref Expression
Assertion tospos 
|- ( F e. Toset -> F e. Poset )

Proof

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