Definition df-tsr

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

	Ref	Expression
Assertion	df-tsr	$$⊢\mathrm{TosetRel}=\left\{r\in \mathrm{PosetRel}|\mathrm{dom}r\times \mathrm{dom}r\subseteq r\cup r^{-1}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctsr	$$class\mathrm{TosetRel}$$
1		vr	$$setvarr$$
2		cps	$$class\mathrm{PosetRel}$$
3	1	cv	$$setvarr$$
4	3	cdm	$$class\mathrm{dom}r$$
5	4 4	cxp	$$class\left(\mathrm{dom}r\times \mathrm{dom}r\right)$$
6	3	ccnv	$$class{r}^{-1}$$
7	3 6	cun	$$class\left(r\cup r^{-1}\right)$$
8	5 7	wss	$$wff\mathrm{dom}r\times \mathrm{dom}r\subseteq r\cup r^{-1}$$
9	8 1 2	crab	$$class\left\{r\in \mathrm{PosetRel}|\mathrm{dom}r\times \mathrm{dom}r\subseteq r\cup r^{-1}\right\}$$
10	0 9	wceq	$$wff\mathrm{TosetRel}=\left\{r\in \mathrm{PosetRel}|\mathrm{dom}r\times \mathrm{dom}r\subseteq r\cup r^{-1}\right\}$$