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

Definition df-so 4273
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 8857). (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 4271 . 2  wff  R  Or  A
41, 2wpo 4270 . . 3  wff  R  Po  A
5 vx . . . . . . . 8  set  x
65cv 1618 . . . . . . 7  class  x
7 vy . . . . . . . 8  set  y
87cv 1618 . . . . . . 7  class  y
96, 8, 2wbr 3983 . . . . . 6  wff  x R y
105, 7weq 1620 . . . . . 6  wff  x  =  y
118, 6, 2wbr 3983 . . . . . 6  wff  y R x
129, 10, 11w3o 938 . . . . 5  wff  ( x R y  \/  x  =  y  \/  y R x )
1312, 7, 1wral 2516 . . . 4  wff  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
1413, 5, 1wral 2516 . . 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  4278  sopo  4289  soss  4290  soeq1  4291  solin  4295  issod  4302  so0  4305  dfwe2  4531  soinxp  4728  sosn  4733  cnvso  5187  isosolem  5764  soxp  6148  sorpss  6202  sornom  7857  zorn2lem6  8082  tosso  14090  dfso3  23432  dfso2  23468  soseq  23609
  Copyright terms: Public domain W3C validator