MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-toset Structured version   Visualization version   GIF version

Definition df-toset 16799
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
StepHypRef Expression
1 ctos 16798 . 2 class Toset
2 vx . . . . . . . . . 10 setvar 𝑥
32cv 1473 . . . . . . . . 9 class 𝑥
4 vy . . . . . . . . . 10 setvar 𝑦
54cv 1473 . . . . . . . . 9 class 𝑦
6 vr . . . . . . . . . 10 setvar 𝑟
76cv 1473 . . . . . . . . 9 class 𝑟
83, 5, 7wbr 4573 . . . . . . . 8 wff 𝑥𝑟𝑦
95, 3, 7wbr 4573 . . . . . . . 8 wff 𝑦𝑟𝑥
108, 9wo 381 . . . . . . 7 wff (𝑥𝑟𝑦𝑦𝑟𝑥)
11 vb . . . . . . . 8 setvar 𝑏
1211cv 1473 . . . . . . 7 class 𝑏
1310, 4, 12wral 2891 . . . . . 6 wff 𝑦𝑏 (𝑥𝑟𝑦𝑦𝑟𝑥)
1413, 2, 12wral 2891 . . . . 5 wff 𝑥𝑏𝑦𝑏 (𝑥𝑟𝑦𝑦𝑟𝑥)
15 vf . . . . . . 7 setvar 𝑓
1615cv 1473 . . . . . 6 class 𝑓
17 cple 15717 . . . . . 6 class le
1816, 17cfv 5786 . . . . 5 class (le‘𝑓)
1914, 6, 18wsbc 3397 . . . 4 wff [(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏 (𝑥𝑟𝑦𝑦𝑟𝑥)
20 cbs 15637 . . . . 5 class Base
2116, 20cfv 5786 . . . 4 class (Base‘𝑓)
2219, 11, 21wsbc 3397 . . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏 (𝑥𝑟𝑦𝑦𝑟𝑥)
23 cpo 16705 . . 3 class Poset
2422, 15, 23crab 2895 . 2 class {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏 (𝑥𝑟𝑦𝑦𝑟𝑥)}
251, 24wceq 1474 1 wff Toset = {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏 (𝑥𝑟𝑦𝑦𝑟𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  istos  16800
  Copyright terms: Public domain W3C validator