Definition df-tsr 16496

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

Assertion

Ref	Expression
df-tsr	|- TosetRel = { r e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) }

Detailed syntax breakdown of Definition df-tsr

Step	Hyp	Ref	Expression
1		ctsr 16494	. 2 class TosetRel
2		vr	. . . . . . 7 setvar r
3	2	cv 1454	. . . . . 6 class r
4	3	cdm 4853	. . . . 5 class dom r
5	4, 4	cxp 4851	. . . 4 class ( dom r X. dom r )
6	3	ccnv 4852	. . . . 5 class `' r
7	3, 6	cun 3414	. . . 4 class ( r u. `' r )
8	5, 7	wss 3416	. . 3 wff ( dom r X. dom r ) C_ ( r u. `' r )
9		cps 16493	. . 3 class PosetRel
10	8, 2, 9	crab 2753	. 2 class { r e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) }
11	1, 10	wceq 1455	1 wff TosetRel = { r e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) }

This definition is referenced by:  istsr  16512