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

Definition df-so 4663
Description: Define the strict complete (linear) order predicate. The expression is true if relationship orders . For example, is true (ltso 9334). 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 4661 . 2
41, 2wpo 4660 . . 3
5 vx . . . . . . . 8
65cv 1669 . . . . . . 7
7 vy . . . . . . . 8
87cv 1669 . . . . . . 7
96, 8, 2wbr 4318 . . . . . 6
105, 7weq 1671 . . . . . 6
118, 6, 2wbr 4318 . . . . . 6
129, 10, 11w3o 938 . . . . 5
1312, 7, 1wral 2759 . . . 4
1413, 5, 1wral 2759 . . 3
154, 14wa 360 . 2
163, 15wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfso  4668  sopo  4679  soss  4680  soeq1  4681  solin  4685  issod  4692  so0  4695  soinxp  4925  sosn  4930  cnvso  5396  isosolem  6048  sorpss  6375  dfwe2  6403  soxp  6691  sornom  8328  zorn2lem6  8552  tosso  15047  dfso3  26516  dfso2  26716  soseq  26868
  Copyright terms: Public domain W3C validator