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 e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctsr	|- TosetRel
1		vr	|- r
2		cps	|- PosetRel
3	1	cv	|- r
4	3	cdm	|- dom r
5	4 4	cxp	|- ( dom r X. dom r )
6	3	ccnv	|- `' r
7	3 6	cun	|- ( r u. `' r )
8	5 7	wss	|- ( dom r X. dom r ) C_ ( r u. `' r )
9	8 1 2	crab	|- { r e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) }
10	0 9	wceq	|- TosetRel = { r e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) }