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

Definition df-iso 4061
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 4059 . 2  wff  R  Or  A
41, 2wpo 4058 . . 3  wff  R  Po  A
5 vx . . . . . . . . 9  setvar  x
65cv 1258 . . . . . . . 8  class  x
7 vy . . . . . . . . 9  setvar  y
87cv 1258 . . . . . . . 8  class  y
96, 8, 2wbr 3791 . . . . . . 7  wff  x R y
10 vz . . . . . . . . . 10  setvar  z
1110cv 1258 . . . . . . . . 9  class  z
126, 11, 2wbr 3791 . . . . . . . 8  wff  x R z
1311, 8, 2wbr 3791 . . . . . . . 8  wff  z R y
1412, 13wo 639 . . . . . . 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 2323 . . . . 5  wff  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1716, 7, 1wral 2323 . . . 4  wff  A. y  e.  A  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1817, 5, 1wral 2323 . . 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 101 . 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 102 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  4066  sopo  4077  soss  4078  soeq1  4079  issod  4083  sowlin  4084  so0  4090  ordsoexmid  4313  soinxp  4437  sosng  4440  cnvsom  4888  isosolem  5490  ltsopr  6751  ltsosr  6906  ltso  7154  xrltso  8817
  Copyright terms: Public domain W3C validator