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

Definition df-so 4806
Description: Define the strict complete (linear) order predicate. The expression is true if relationship orders . For example, is true (ltso 9686). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.)
Assertion
Ref Expression
df-so
Distinct variable groups:   , ,   , ,

Detailed syntax breakdown of Definition df-so
StepHypRef Expression
1 cA . . 3
2 cR . . 3
31, 2wor 4804 . 2
41, 2wpo 4803 . . 3
5 vx . . . . . . . 8
65cv 1394 . . . . . . 7
7 vy . . . . . . . 8
87cv 1394 . . . . . . 7
96, 8, 2wbr 4452 . . . . . 6
105, 7weq 1733 . . . . . 6
118, 6, 2wbr 4452 . . . . . 6
129, 10, 11w3o 972 . . . . 5
1312, 7, 1wral 2807 . . . 4
1413, 5, 1wral 2807 . . 3
154, 14wa 369 . 2
163, 15wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  nfso  4811  sopo  4822  soss  4823  soeq1  4824  solin  4828  issod  4835  so0  4838  soinxp  5069  sosn  5074  cnvso  5551  isosolem  6243  sorpss  6585  dfwe2  6617  soxp  6913  sornom  8678  zorn2lem6  8902  tosso  15666  dfso3  29097  dfso2  29183  soseq  29334
  Copyright terms: Public domain W3C validator