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

Definition df-iso 4189
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 4187 . 2  wff  R  Or  A
41, 2wpo 4186 . . 3  wff  R  Po  A
5 vx . . . . . . . . 9  setvar  x
65cv 1315 . . . . . . . 8  class  x
7 vy . . . . . . . . 9  setvar  y
87cv 1315 . . . . . . . 8  class  y
96, 8, 2wbr 3899 . . . . . . 7  wff  x R y
10 vz . . . . . . . . . 10  setvar  z
1110cv 1315 . . . . . . . . 9  class  z
126, 11, 2wbr 3899 . . . . . . . 8  wff  x R z
1311, 8, 2wbr 3899 . . . . . . . 8  wff  z R y
1412, 13wo 682 . . . . . . 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 2393 . . . . 5  wff  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1716, 7, 1wral 2393 . . . 4  wff  A. y  e.  A  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1817, 5, 1wral 2393 . . 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 103 . 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 104 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  4194  sopo  4205  soss  4206  soeq1  4207  issod  4211  sowlin  4212  so0  4218  ordsoexmid  4447  soinxp  4579  sosng  4582  cnvsom  5052  isosolem  5693  ltsopr  7372  ltsosr  7540  ltso  7810  xrltso  9537
  Copyright terms: Public domain W3C validator