ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-iso Unicode version

Definition df-iso 4081
Description: Define the strict linear order predicate. The expression  R  Or  A is true if relationship  R orders  A. The property  x R y  ->  ( x R z  \/  z R y ) is called weak linearity by Proposition 11.2.3 of [HoTT], p. (varies). If we assumed excluded middle, it would be equivalent to trichotomy, 
x R y  \/  x  =  y  \/  y R x. (Contributed by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
Assertion
Ref Expression
df-iso  |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) ) ) )
Distinct variable groups:    x, y, z, R    x, A, y, z

Detailed syntax breakdown of Definition df-iso
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2wor 4079 . 2  wff  R  Or  A
41, 2wpo 4078 . . 3  wff  R  Po  A
5 vx . . . . . . . . 9  setvar  x
65cv 1284 . . . . . . . 8  class  x
7 vy . . . . . . . . 9  setvar  y
87cv 1284 . . . . . . . 8  class  y
96, 8, 2wbr 3806 . . . . . . 7  wff  x R y
10 vz . . . . . . . . . 10  setvar  z
1110cv 1284 . . . . . . . . 9  class  z
126, 11, 2wbr 3806 . . . . . . . 8  wff  x R z
1311, 8, 2wbr 3806 . . . . . . . 8  wff  z R y
1412, 13wo 662 . . . . . . 7  wff  ( x R z  \/  z R y )
159, 14wi 4 . . . . . 6  wff  ( x R y  ->  (
x R z  \/  z R y ) )
1615, 10, 1wral 2353 . . . . 5  wff  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1716, 7, 1wral 2353 . . . 4  wff  A. y  e.  A  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1817, 5, 1wral 2353 . . 3  wff  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
194, 18wa 102 . 2  wff  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  (
x R y  -> 
( x R z  \/  z R y ) ) )
203, 19wb 103 1  wff  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  nfso  4086  sopo  4097  soss  4098  soeq1  4099  issod  4103  sowlin  4104  so0  4110  ordsoexmid  4334  soinxp  4457  sosng  4460  cnvsom  4912  isosolem  5516  ltsopr  6925  ltsosr  7080  ltso  7333  xrltso  9024
  Copyright terms: Public domain W3C validator