Definition df-toset 16857

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

Assertion

Ref	Expression
df-toset	⊢ Toset = {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)}

Distinct variable group:   𝑓,𝑏,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-toset

Step	Hyp	Ref	Expression
1		ctos 16856	. 2 class Toset
2		vx	. . . . . . . . . 10 setvar 𝑥
3	2	cv 1474	. . . . . . . . 9 class 𝑥
4		vy	. . . . . . . . . 10 setvar 𝑦
5	4	cv 1474	. . . . . . . . 9 class 𝑦
6		vr	. . . . . . . . . 10 setvar 𝑟
7	6	cv 1474	. . . . . . . . 9 class 𝑟
8	3, 5, 7	wbr 4583	. . . . . . . 8 wff 𝑥𝑟𝑦
9	5, 3, 7	wbr 4583	. . . . . . . 8 wff 𝑦𝑟𝑥
10	8, 9	wo 382	. . . . . . 7 wff (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
11		vb	. . . . . . . 8 setvar 𝑏
12	11	cv 1474	. . . . . . 7 class 𝑏
13	10, 4, 12	wral 2896	. . . . . 6 wff ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
14	13, 2, 12	wral 2896	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
15		vf	. . . . . . 7 setvar 𝑓
16	15	cv 1474	. . . . . 6 class 𝑓
17		cple 15775	. . . . . 6 class le
18	16, 17	cfv 5804	. . . . 5 class (le‘𝑓)
19	14, 6, 18	wsbc 3402	. . . 4 wff [(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
20		cbs 15695	. . . . 5 class Base
21	16, 20	cfv 5804	. . . 4 class (Base‘𝑓)
22	19, 11, 21	wsbc 3402	. . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
23		cpo 16763	. . 3 class Poset
24	22, 15, 23	crab 2900	. 2 class {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)}
25	1, 24	wceq 1475	1 wff Toset = {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)}

This definition is referenced by:  istos  16858