Definition df-toset

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

	Ref	Expression
Assertion	df-toset	$$⊢\mathrm{Toset}=\left\{f\in \mathrm{Poset}|\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctos	$$class\mathrm{Toset}$$
1		vf	$$setvarf$$
2		cpo	$$class\mathrm{Poset}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarf$$
5	4 3	cfv	$$class{\mathrm{Base}}_f$$
6		vb	$$setvarb$$
7		cple	$$class\mathrm{le}$$
8	4 7	cfv	$$class{\le }_f$$
9		vr	$$setvarr$$
10		vx	$$setvarx$$
11	6	cv	$$setvarb$$
12		vy	$$setvary$$
13	10	cv	$$setvarx$$
14	9	cv	$$setvarr$$
15	12	cv	$$setvary$$
16	13 15 14	wbr	$$wffxry$$
17	15 13 14	wbr	$$wffyrx$$
18	16 17	wo	$$wff\left(xry\vee yrx\right)$$
19	18 12 11	wral	$$wff\forall y\in b\left(xry\vee yrx\right)$$
20	19 10 11	wral	$$wff\forall x\in b\forall y\in b\left(xry\vee yrx\right)$$
21	20 9 8	wsbc	$$wff\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)$$
22	21 6 5	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)$$
23	22 1 2	crab	$$class\left\{f\in \mathrm{Poset}|\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\right\}$$
24	0 23	wceq	$$wff\mathrm{Toset}=\left\{f\in \mathrm{Poset}|\underset{\dot{}}{[}{\mathrm{Base}}_f/b\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_f/r\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xry\vee yrx\right)\right\}$$