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

Metamath Proof Explorer

Theorem tsrps

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

Ref Expression
Assertion tsrps ( 𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel )

Proof

Step Hyp Ref Expression
1 eqid ⊢ dom 𝑅 = dom 𝑅
2 1 istsr ⊢ ( 𝑅 ∈ TosetRel ↔ ( 𝑅 ∈ PosetRel ∧ ( dom 𝑅 × dom 𝑅 ) ⊆ ( 𝑅 ∪ ◡ 𝑅 ) ) )
3 2 simplbi ⊢ ( 𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel )