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

Definition df-so 4506
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 9158). 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 4504 . 2  wff  R  Or  A
41, 2wpo 4503 . . 3  wff  R  Po  A
5 vx . . . . . . . 8  set  x
65cv 1652 . . . . . . 7  class  x
7 vy . . . . . . . 8  set  y
87cv 1652 . . . . . . 7  class  y
96, 8, 2wbr 4214 . . . . . 6  wff  x R y
105, 7weq 1654 . . . . . 6  wff  x  =  y
118, 6, 2wbr 4214 . . . . . 6  wff  y R x
129, 10, 11w3o 936 . . . . 5  wff  ( x R y  \/  x  =  y  \/  y R x )
1312, 7, 1wral 2707 . . . 4  wff  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
1413, 5, 1wral 2707 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
154, 14wa 360 . 2  wff  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) )
163, 15wb 178 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  4511  sopo  4522  soss  4523  soeq1  4524  solin  4528  issod  4535  so0  4538  dfwe2  4764  soinxp  4944  sosn  4949  cnvso  5413  isosolem  6069  soxp  6461  sorpss  6529  sornom  8159  zorn2lem6  8383  tosso  14467  dfso3  25179  dfso2  25379  soseq  25531
  Copyright terms: Public domain W3C validator