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

Definition df-so 4331
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 8919). 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 4329 . 2  wff  R  Or  A
41, 2wpo 4328 . . 3  wff  R  Po  A
5 vx . . . . . . . 8  set  x
65cv 1631 . . . . . . 7  class  x
7 vy . . . . . . . 8  set  y
87cv 1631 . . . . . . 7  class  y
96, 8, 2wbr 4039 . . . . . 6  wff  x R y
105, 7weq 1633 . . . . . 6  wff  x  =  y
118, 6, 2wbr 4039 . . . . . 6  wff  y R x
129, 10, 11w3o 933 . . . . 5  wff  ( x R y  \/  x  =  y  \/  y R x )
1312, 7, 1wral 2556 . . . 4  wff  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )
1413, 5, 1wral 2556 . . 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  4336  sopo  4347  soss  4348  soeq1  4349  solin  4353  issod  4360  so0  4363  dfwe2  4589  soinxp  4770  sosn  4775  cnvso  5230  isosolem  5860  soxp  6244  sorpss  6298  sornom  7919  zorn2lem6  8144  tosso  14158  dfso3  24089  dfso2  24182  soseq  24325
  Copyright terms: Public domain W3C validator