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

Definition df-so 4438
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 9082). 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 4436 . 2  wff  R  Or  A
41, 2wpo 4435 . . 3  wff  R  Po  A
5 vx . . . . . . . 8  set  x
65cv 1648 . . . . . . 7  class  x
7 vy . . . . . . . 8  set  y
87cv 1648 . . . . . . 7  class  y
96, 8, 2wbr 4146 . . . . . 6  wff  x R y
105, 7weq 1650 . . . . . 6  wff  x  =  y
118, 6, 2wbr 4146 . . . . . 6  wff  y R x
129, 10, 11w3o 935 . . . . 5  wff  ( x R y  \/  x  =  y  \/  y R x )
1312, 7, 1wral 2642 . . . 4  wff  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
1413, 5, 1wral 2642 . . 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  4443  sopo  4454  soss  4455  soeq1  4456  solin  4460  issod  4467  so0  4470  dfwe2  4695  soinxp  4875  sosn  4880  cnvso  5344  isosolem  5999  soxp  6388  sorpss  6456  sornom  8083  zorn2lem6  8307  tosso  14385  dfso3  24949  dfso2  25128  soseq  25271
  Copyright terms: Public domain W3C validator