Definition df-toset 15988

Description: Define the class of totally ordered sets (tosets). (Contributed by FL, 17-Nov-2014.)

Assertion

Ref	Expression
df-toset	|- Toset = { f e. Poset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) }

Distinct variable group:   f, b, r, x, y

Detailed syntax breakdown of Definition df-toset

Step	Hyp	Ref	Expression
1		ctos 15987	. 2 class Toset
2		vx	. . . . . . . . . 10 setvar x
3	2	cv 1404	. . . . . . . . 9 class x
4		vy	. . . . . . . . . 10 setvar y
5	4	cv 1404	. . . . . . . . 9 class y
6		vr	. . . . . . . . . 10 setvar r
7	6	cv 1404	. . . . . . . . 9 class r
8	3, 5, 7	wbr 4395	. . . . . . . 8 wff x r y
9	5, 3, 7	wbr 4395	. . . . . . . 8 wff y r x
10	8, 9	wo 366	. . . . . . 7 wff ( x r y \/ y r x )
11		vb	. . . . . . . 8 setvar b
12	11	cv 1404	. . . . . . 7 class b
13	10, 4, 12	wral 2754	. . . . . 6 wff A. y e. b ( x r y \/ y r x )
14	13, 2, 12	wral 2754	. . . . 5 wff A. x e. b A. y e. b ( x r y \/ y r x )
15		vf	. . . . . . 7 setvar f
16	15	cv 1404	. . . . . 6 class f
17		cple 14916	. . . . . 6 class le
18	16, 17	cfv 5569	. . . . 5 class ( le ` f )
19	14, 6, 18	wsbc 3277	. . . 4 wff [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x )
20		cbs 14841	. . . . 5 class Base
21	16, 20	cfv 5569	. . . 4 class ( Base ` f )
22	19, 11, 21	wsbc 3277	. . 3 wff [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x )
23		cpo 15893	. . 3 class Poset
24	22, 15, 23	crab 2758	. 2 class { f e. Poset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) }
25	1, 24	wceq 1405	1 wff Toset = { f e. Poset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) }

This definition is referenced by:  istos  15989