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

Definition df-so 4545
Description: Define the strict complete (linear) order predicate. The expression is true if relationship orders . For example, ?Error: < Or RR ^ This math symbol is not active (i.e. was not declared in this scope). Or is true (ltso 9207). 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 4543 . 2
41, 2wpo 4542 . . 3
5 vx . . . . . . . 8
65cv 1653 . . . . . . 7
7 vy . . . . . . . 8
87cv 1653 . . . . . . 7
96, 8, 2wbr 4243 . . . . . 6
105, 7weq 1655 . . . . . 6
118, 6, 2wbr 4243 . . . . . 6
129, 10, 11w3o 936 . . . . 5
1312, 7, 1wral 2712 . . . 4
1413, 5, 1wral 2712 . . 3
154, 14wa 360 . 2
163, 15wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfso  4550  sopo  4561  soss  4562  soeq1  4563  solin  4567  issod  4574  so0  4577  dfwe2  4803  soinxp  4982  sosn  4987  cnvso  5457  isosolem  6115  soxp  6509  sorpss  6577  sornom  8208  zorn2lem6  8432  tosso  14516  dfso3  25281  dfso2  25481  soseq  25633
  Copyright terms: Public domain W3C validator