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

Definition df-so 4315
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 8903). 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 4313 . 2  wff  R  Or  A
41, 2wpo 4312 . . 3  wff  R  Po  A
5 vx . . . . . . . 8  set  x
65cv 1622 . . . . . . 7  class  x
7 vy . . . . . . . 8  set  y
87cv 1622 . . . . . . 7  class  y
96, 8, 2wbr 4023 . . . . . 6  wff  x R y
105, 7weq 1624 . . . . . 6  wff  x  =  y
118, 6, 2wbr 4023 . . . . . 6  wff  y R x
129, 10, 11w3o 933 . . . . 5  wff  ( x R y  \/  x  =  y  \/  y R x )
1312, 7, 1wral 2543 . . . 4  wff  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
1413, 5, 1wral 2543 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
154, 14wa 358 . 2  wff  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) )
163, 15wb 176 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  4320  sopo  4331  soss  4332  soeq1  4333  solin  4337  issod  4344  so0  4347  dfwe2  4573  soinxp  4754  sosn  4759  cnvso  5214  isosolem  5844  soxp  6228  sorpss  6282  sornom  7903  zorn2lem6  8128  tosso  14142  dfso3  24074  dfso2  24111  soseq  24254
  Copyright terms: Public domain W3C validator