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

Definition df-so 4496
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 9145). 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 4494 . 2  wff  R  Or  A
41, 2wpo 4493 . . 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 4204 . . . . . 6  wff  x R y
105, 7weq 1653 . . . . . 6  wff  x  =  y
118, 6, 2wbr 4204 . . . . . 6  wff  y R x
129, 10, 11w3o 935 . . . . 5  wff  ( x R y  \/  x  =  y  \/  y R x )
1312, 7, 1wral 2697 . . . 4  wff  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
1413, 5, 1wral 2697 . . 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  4501  sopo  4512  soss  4513  soeq1  4514  solin  4518  issod  4525  so0  4528  dfwe2  4753  soinxp  4933  sosn  4938  cnvso  5402  isosolem  6058  soxp  6450  sorpss  6518  sornom  8146  zorn2lem6  8370  tosso  14453  dfso3  25165  dfso2  25366  soseq  25509
  Copyright terms: Public domain W3C validator