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

Metamath Proof Explorer

Definition df-tsr

Description: Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009)

Ref Expression
Assertion df-tsr ⊢ TosetRel = r ∈ PosetRel | dom ⁡ r × dom ⁡ r ⊆ r ∪ r -1

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctsr class TosetRel
1 vr setvar r
2 cps class PosetRel
3 1 cv setvar r
4 3 cdm class dom ⁡ r
5 4 4 cxp class dom ⁡ r × dom ⁡ r
6 3 ccnv class r -1
7 3 6 cun class r ∪ r -1
8 5 7 wss wff dom ⁡ r × dom ⁡ r ⊆ r ∪ r -1
9 8 1 2 crab class r ∈ PosetRel | dom ⁡ r × dom ⁡ r ⊆ r ∪ r -1
10 0 9 wceq wff TosetRel = r ∈ PosetRel | dom ⁡ r × dom ⁡ r ⊆ r ∪ r -1