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

Definition df-iso 4031
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 4029 . 2  wff  R  Or  A
41, 2wpo 4028 . . 3  wff  R  Po  A
5 vx . . . . . . . . 9  setvar  x
65cv 1242 . . . . . . . 8  class  x
7 vy . . . . . . . . 9  setvar  y
87cv 1242 . . . . . . . 8  class  y
96, 8, 2wbr 3761 . . . . . . 7  wff  x R y
10 vz . . . . . . . . . 10  setvar  z
1110cv 1242 . . . . . . . . 9  class  z
126, 11, 2wbr 3761 . . . . . . . 8  wff  x R z
1311, 8, 2wbr 3761 . . . . . . . 8  wff  z R y
1412, 13wo 629 . . . . . . 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 2303 . . . . 5  wff  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1716, 7, 1wral 2303 . . . 4  wff  A. y  e.  A  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1817, 5, 1wral 2303 . . 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 97 . 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 98 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  4036  sopo  4047  soss  4048  soeq1  4049  issod  4053  sowlin  4054  so0  4060  ordsoexmid  4271  soinxp  4388  sosng  4391  cnvsom  4839  isosolem  5441  ltsopr  6666  ltsosr  6821  ltso  7067  xrltso  8675
  Copyright terms: Public domain W3C validator