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

Definition df-so 4759
Description: Define the strict complete (linear) order predicate. The expression is true if relationship orders . For example, is true (ltso 9592). 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 4757 . 2
41, 2wpo 4756 . . 3
5 vx . . . . . . . 8
65cv 1369 . . . . . . 7
7 vy . . . . . . . 8
87cv 1369 . . . . . . 7
96, 8, 2wbr 4409 . . . . . 6
105, 7weq 1696 . . . . . 6
118, 6, 2wbr 4409 . . . . . 6
129, 10, 11w3o 964 . . . . 5
1312, 7, 1wral 2800 . . . 4
1413, 5, 1wral 2800 . . 3
154, 14wa 369 . 2
163, 15wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  nfso  4764  sopo  4775  soss  4776  soeq1  4777  solin  4781  issod  4788  so0  4791  soinxp  5020  sosn  5025  cnvso  5495  isosolem  6169  sorpss  6498  dfwe2  6526  soxp  6819  sornom  8583  zorn2lem6  8807  tosso  15365  legso  23448  dfso3  27832  dfso2  28020  soseq  28171
  Copyright terms: Public domain W3C validator