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

Definition df-so 4645
Description: Define the strict complete (linear) order predicate. The expression is true if relationship orders . For example, is true (ltso 9277). 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 4643 . 2
41, 2wpo 4642 . . 3
5 vx . . . . . . . 8
65cv 1661 . . . . . . 7
7 vy . . . . . . . 8
87cv 1661 . . . . . . 7
96, 8, 2wbr 4302 . . . . . 6
105, 7weq 1663 . . . . . 6
118, 6, 2wbr 4302 . . . . . 6
129, 10, 11w3o 938 . . . . 5
1312, 7, 1wral 2751 . . . 4
1413, 5, 1wral 2751 . . 3
154, 14wa 360 . 2
163, 15wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfso  4650  sopo  4661  soss  4662  soeq1  4663  solin  4667  issod  4674  so0  4677  soinxp  4907  sosn  4912  cnvso  5375  isosolem  6012  sorpss  6331  dfwe2  6358  soxp  6642  sornom  8271  zorn2lem6  8495  tosso  14984  dfso3  26007  dfso2  26207  soseq  26359
  Copyright terms: Public domain W3C validator