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

Definition df-toset 16218
 Description: Define the class of totally ordered sets (tosets). (Contributed by FL, 17-Nov-2014.)
Assertion
Ref Expression
df-toset Toset
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-toset
StepHypRef Expression
1 ctos 16217 . 2 Toset
2 vx . . . . . . . . . 10
32cv 1436 . . . . . . . . 9
4 vy . . . . . . . . . 10
54cv 1436 . . . . . . . . 9
6 vr . . . . . . . . . 10
76cv 1436 . . . . . . . . 9
83, 5, 7wbr 4361 . . . . . . . 8
95, 3, 7wbr 4361 . . . . . . . 8
108, 9wo 369 . . . . . . 7
11 vb . . . . . . . 8
1211cv 1436 . . . . . . 7
1310, 4, 12wral 2709 . . . . . 6
1413, 2, 12wral 2709 . . . . 5
15 vf . . . . . . 7
1615cv 1436 . . . . . 6
17 cple 15135 . . . . . 6
1816, 17cfv 5539 . . . . 5
1914, 6, 18wsbc 3237 . . . 4
20 cbs 15059 . . . . 5
2116, 20cfv 5539 . . . 4
2219, 11, 21wsbc 3237 . . 3
23 cpo 16123 . . 3
2422, 15, 23crab 2713 . 2
251, 24wceq 1437 1 Toset
 Colors of variables: wff setvar class This definition is referenced by:  istos  16219
 Copyright terms: Public domain W3C validator