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

Definition df-toset 14463
 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 14462 . 2 Toset
2 vx . . . . . . . . . 10
32cv 1651 . . . . . . . . 9
4 vy . . . . . . . . . 10
54cv 1651 . . . . . . . . 9
6 vr . . . . . . . . . 10
76cv 1651 . . . . . . . . 9
83, 5, 7wbr 4212 . . . . . . . 8
95, 3, 7wbr 4212 . . . . . . . 8
108, 9wo 358 . . . . . . 7
11 vb . . . . . . . 8
1211cv 1651 . . . . . . 7
1310, 4, 12wral 2705 . . . . . 6
1413, 2, 12wral 2705 . . . . 5
15 vf . . . . . . 7
1615cv 1651 . . . . . 6
17 cple 13536 . . . . . 6
1816, 17cfv 5454 . . . . 5
1914, 6, 18wsbc 3161 . . . 4
20 cbs 13469 . . . . 5
2116, 20cfv 5454 . . . 4
2219, 11, 21wsbc 3161 . . 3
23 cpo 14397 . . 3
2422, 15, 23crab 2709 . 2
251, 24wceq 1652 1 Toset
 Colors of variables: wff set class This definition is referenced by:  istos  14464
 Copyright terms: Public domain W3C validator