Metamath Proof Explorer

Theorem tsrps

Description: A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion tsrps 
|- ( R e. TosetRel -> R e. PosetRel )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  dom R = dom R
2 1 istsr 
 |-  ( R e. TosetRel <-> ( R e. PosetRel /\ ( dom R X. dom R ) C_ ( R u. `' R ) ) )
3 2 simplbi 
 |-  ( R e. TosetRel -> R e. PosetRel )