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

Definition df-iso 4299
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 4297 . 2  wff  R  Or  A
41, 2wpo 4296 . . 3  wff  R  Po  A
5 vx . . . . . . . . 9  setvar  x
65cv 1352 . . . . . . . 8  class  x
7 vy . . . . . . . . 9  setvar  y
87cv 1352 . . . . . . . 8  class  y
96, 8, 2wbr 4005 . . . . . . 7  wff  x R y
10 vz . . . . . . . . . 10  setvar  z
1110cv 1352 . . . . . . . . 9  class  z
126, 11, 2wbr 4005 . . . . . . . 8  wff  x R z
1311, 8, 2wbr 4005 . . . . . . . 8  wff  z R y
1412, 13wo 708 . . . . . . 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 2455 . . . . 5  wff  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1716, 7, 1wral 2455 . . . 4  wff  A. y  e.  A  A. z  e.  A  ( x R y  ->  (
x R z  \/  z R y ) )
1817, 5, 1wral 2455 . . 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 104 . 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 105 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  4304  sopo  4315  soss  4316  soeq1  4317  issod  4321  sowlin  4322  so0  4328  ordsoexmid  4563  soinxp  4698  sosng  4701  cnvsom  5174  isosolem  5828  ltsopr  7598  ltsosr  7766  ltso  8038  xrltso  9799
  Copyright terms: Public domain W3C validator