Definition df-toset

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctos	⊢ Toset
1		vf	⊢ 𝑓
2		cpo	⊢ Poset
3		cbs	⊢ Base
4	1	cv	⊢ 𝑓
5	4 3	cfv	⊢ ( Base ‘ 𝑓 )
6		vb	⊢ 𝑏
7		cple	⊢ le
8	4 7	cfv	⊢ ( le ‘ 𝑓 )
9		vr	⊢ 𝑟
10		vx	⊢ 𝑥
11	6	cv	⊢ 𝑏
12		vy	⊢ 𝑦
13	10	cv	⊢ 𝑥
14	9	cv	⊢ 𝑟
15	12	cv	⊢ 𝑦
16	13 15 14	wbr	⊢ 𝑥 𝑟 𝑦
17	15 13 14	wbr	⊢ 𝑦 𝑟 𝑥
18	16 17	wo	⊢ ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
19	18 12 11	wral	⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
20	19 10 11	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
21	20 9 8	wsbc	⊢ [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
22	21 6 5	wsbc	⊢ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
23	22 1 2	crab	⊢ { 𝑓 ∈ Poset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) }
24	0 23	wceq	⊢ Toset = { 𝑓 ∈ Poset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) }