Metamath Proof Explorer


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 ‘ 𝑓 ) / 𝑟 ]𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) }