MPE Home 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  R  Or  A is true if relationship  R orders  A. For example,  <  Or  RR 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  |-  ( 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 4462 . 2  wff  R  Or  A
41, 2wpo 4461 . . 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 4172 . . . . . 6  wff  x R y
105, 7weq 1650 . . . . . 6  wff  x  =  y
118, 6, 2wbr 4172 . . . . . 6  wff  y R x
129, 10, 11w3o 935 . . . . 5  wff  ( x R y  \/  x  =  y  \/  y R x )
1312, 7, 1wral 2666 . . . 4  wff  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
1413, 5, 1wral 2666 . . 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  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