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

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

Detailed syntax breakdown of Definition df-iso
StepHypRef Expression
1 cA . . 3
2 cR . . 3  R
31, 2wor 4023 . 2  R  Or
41, 2wpo 4022 . . 3  R  Po
5 vx . . . . . . . . 9  setvar
65cv 1241 . . . . . . . 8
7 vy . . . . . . . . 9  setvar
87cv 1241 . . . . . . . 8
96, 8, 2wbr 3755 . . . . . . 7  R
10 vz . . . . . . . . . 10  setvar
1110cv 1241 . . . . . . . . 9
126, 11, 2wbr 3755 . . . . . . . 8  R
1311, 8, 2wbr 3755 . . . . . . . 8  R
1412, 13wo 628 . . . . . . 7  R  R
159, 14wi 4 . . . . . 6  R  R  R
1615, 10, 1wral 2300 . . . . 5  R  R  R
1716, 7, 1wral 2300 . . . 4  R  R  R
1817, 5, 1wral 2300 . . 3  R  R  R
194, 18wa 97 . 2  R  Po  R  R  R
203, 19wb 98 1  R  Or  R  Po  R  R  R
Colors of variables: wff set class
This definition is referenced by:  nfso  4030  sopo  4041  soss  4042  soeq1  4043  issod  4047  sowlin  4048  so0  4054  ordsoexmid  4240  soinxp  4353  sosng  4356  cnvsom  4804  isosolem  5406  ltsopr  6570  ltsosr  6692  ltso  6893  xrltso  8487
  Copyright terms: Public domain W3C validator