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 )