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

Definition df-so 4464
 Description: Define the strict complete (linear) order predicate. The expression is true if relationship orders . For example, is true (ltso 9112). 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 4462 . 2
41, 2wpo 4461 . . 3
5 vx . . . . . . . 8
65cv 1648 . . . . . . 7
7 vy . . . . . . . 8
87cv 1648 . . . . . . 7
96, 8, 2wbr 4172 . . . . . 6
105, 7weq 1650 . . . . . 6
118, 6, 2wbr 4172 . . . . . 6
129, 10, 11w3o 935 . . . . 5
1312, 7, 1wral 2666 . . . 4
1413, 5, 1wral 2666 . . 3
154, 14wa 359 . 2
163, 15wb 177 1
 Colors of variables: wff set class This definition is referenced by:  nfso  4469  sopo  4480  soss  4481  soeq1  4482  solin  4486  issod  4493  so0  4496  dfwe2  4721  soinxp  4901  sosn  4906  cnvso  5370  isosolem  6026  soxp  6418  sorpss  6486  sornom  8113  zorn2lem6  8337  tosso  14420  dfso3  25130  dfso2  25325  soseq  25468
 Copyright terms: Public domain W3C validator