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

Definition df-so 4613
Description: Define the strict complete (linear) order predicate. The expression is true if relationship orders . For example, is true (ltso 9401). 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 4611 . 2
41, 2wpo 4610 . . 3
5 vx . . . . . . . 8
65cv 1686 . . . . . . 7
7 vy . . . . . . . 8
87cv 1686 . . . . . . 7
96, 8, 2wbr 4267 . . . . . 6
105, 7weq 1688 . . . . . 6
118, 6, 2wbr 4267 . . . . . 6
129, 10, 11w3o 949 . . . . 5
1312, 7, 1wral 2694 . . . 4
1413, 5, 1wral 2694 . . 3
154, 14wa 362 . 2
163, 15wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  nfso  4618  sopo  4629  soss  4630  soeq1  4631  solin  4635  issod  4642  so0  4645  soinxp  4874  sosn  4879  cnvso  5348  isosolem  6006  sorpss  6335  dfwe2  6363  soxp  6654  sornom  8393  zorn2lem6  8617  tosso  15146  dfso3  27078  dfso2  27266  soseq  27417
  Copyright terms: Public domain W3C validator