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

Definition df-so 4316
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 8900). 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 4314 . 2  wff  R  Or  A
41, 2wpo 4313 . . 3  wff  R  Po  A
5 vx . . . . . . . 8  set  x
65cv 1624 . . . . . . 7  class  x
7 vy . . . . . . . 8  set  y
87cv 1624 . . . . . . 7  class  y
96, 8, 2wbr 4026 . . . . . 6  wff  x R y
105, 7weq 1626 . . . . . 6  wff  x  =  y
118, 6, 2wbr 4026 . . . . . 6  wff  y R x
129, 10, 11w3o 935 . . . . 5  wff  ( x R y  \/  x  =  y  \/  y R x )
1312, 7, 1wral 2546 . . . 4  wff  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
1413, 5, 1wral 2546 . . 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  4321  sopo  4332  soss  4333  soeq1  4334  solin  4338  issod  4345  so0  4348  dfwe2  4574  soinxp  4755  sosn  4760  cnvso  5214  isosolem  5807  soxp  6191  sorpss  6245  sornom  7900  zorn2lem6  8125  tosso  14138  dfso3  23480  dfso2  23516  soseq  23657
  Copyright terms: Public domain W3C validator