Definition df-toset 17638

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 17637	. 2 class Toset
2		vx	. . . . . . . . . 10 setvar 𝑥
3	2	cv 1532	. . . . . . . . 9 class 𝑥
4		vy	. . . . . . . . . 10 setvar 𝑦
5	4	cv 1532	. . . . . . . . 9 class 𝑦
6		vr	. . . . . . . . . 10 setvar 𝑟
7	6	cv 1532	. . . . . . . . 9 class 𝑟
8	3, 5, 7	wbr 5058	. . . . . . . 8 wff 𝑥𝑟𝑦
9	5, 3, 7	wbr 5058	. . . . . . . 8 wff 𝑦𝑟𝑥
10	8, 9	wo 843	. . . . . . 7 wff (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
11		vb	. . . . . . . 8 setvar 𝑏
12	11	cv 1532	. . . . . . 7 class 𝑏
13	10, 4, 12	wral 3138	. . . . . 6 wff ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
14	13, 2, 12	wral 3138	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
15		vf	. . . . . . 7 setvar 𝑓
16	15	cv 1532	. . . . . 6 class 𝑓
17		cple 16566	. . . . . 6 class le
18	16, 17	cfv 6349	. . . . 5 class (le‘𝑓)
19	14, 6, 18	wsbc 3771	. . . 4 wff [(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
20		cbs 16477	. . . . 5 class Base
21	16, 20	cfv 6349	. . . 4 class (Base‘𝑓)
22	19, 11, 21	wsbc 3771	. . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)
23		cpo 17544	. . 3 class Poset
24	22, 15, 23	crab 3142	. 2 class {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)}
25	1, 24	wceq 1533	1 wff Toset = {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)}

This definition is referenced by:  istos  17639