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

Definition df-so 4504
Description: Define the strict complete (linear) order predicate. The expression  R  Or  A is true if relationship  R orders  A. For example,  <  Or  RR is true (ltso 9156). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.)
Assertion
Ref Expression
df-so  |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
Distinct variable groups:    x, y, R    x, A, y

Detailed syntax breakdown of Definition df-so
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2wor 4502 . 2  wff  R  Or  A
41, 2wpo 4501 . . 3  wff  R  Po  A
5 vx . . . . . . . 8  set  x
65cv 1651 . . . . . . 7  class  x
7 vy . . . . . . . 8  set  y
87cv 1651 . . . . . . 7  class  y
96, 8, 2wbr 4212 . . . . . 6  wff  x R y
105, 7weq 1653 . . . . . 6  wff  x  =  y
118, 6, 2wbr 4212 . . . . . 6  wff  y R x
129, 10, 11w3o 935 . . . . 5  wff  ( x R y  \/  x  =  y  \/  y R x )
1312, 7, 1wral 2705 . . . 4  wff  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
1413, 5, 1wral 2705 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
154, 14wa 359 . 2  wff  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) )
163, 15wb 177 1  wff  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
Colors of variables: wff set class
This definition is referenced by:  nfso  4509  sopo  4520  soss  4521  soeq1  4522  solin  4526  issod  4533  so0  4536  dfwe2  4762  soinxp  4942  sosn  4947  cnvso  5411  isosolem  6067  soxp  6459  sorpss  6527  sornom  8157  zorn2lem6  8381  tosso  14465  dfso3  25177  dfso2  25377  soseq  25529
  Copyright terms: Public domain W3C validator