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

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

Detailed syntax breakdown of Definition df-iso
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wor 4085 . 2 wff 𝑅 Or 𝐴
41, 2wpo 4084 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1284 . . . . . . . 8 class 𝑥
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1284 . . . . . . . 8 class 𝑦
96, 8, 2wbr 3811 . . . . . . 7 wff 𝑥𝑅𝑦
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1284 . . . . . . . . 9 class 𝑧
126, 11, 2wbr 3811 . . . . . . . 8 wff 𝑥𝑅𝑧
1311, 8, 2wbr 3811 . . . . . . . 8 wff 𝑧𝑅𝑦
1412, 13wo 662 . . . . . . 7 wff (𝑥𝑅𝑧𝑧𝑅𝑦)
159, 14wi 4 . . . . . 6 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1615, 10, 1wral 2353 . . . . 5 wff 𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1716, 7, 1wral 2353 . . . 4 wff 𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1817, 5, 1wral 2353 . . 3 wff 𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
194, 18wa 102 . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))
203, 19wb 103 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))
Colors of variables: wff set class
This definition is referenced by:  nfso  4092  sopo  4103  soss  4104  soeq1  4105  issod  4109  sowlin  4110  so0  4116  ordsoexmid  4340  soinxp  4464  sosng  4467  cnvsom  4926  isosolem  5540  ltsopr  7056  ltsosr  7211  ltso  7464  xrltso  9159
  Copyright terms: Public domain W3C validator