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

Definition df-iso 4148
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 4146 . 2 wff 𝑅 Or 𝐴
41, 2wpo 4145 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1295 . . . . . . . 8 class 𝑥
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1295 . . . . . . . 8 class 𝑦
96, 8, 2wbr 3867 . . . . . . 7 wff 𝑥𝑅𝑦
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1295 . . . . . . . . 9 class 𝑧
126, 11, 2wbr 3867 . . . . . . . 8 wff 𝑥𝑅𝑧
1311, 8, 2wbr 3867 . . . . . . . 8 wff 𝑧𝑅𝑦
1412, 13wo 667 . . . . . . 7 wff (𝑥𝑅𝑧𝑧𝑅𝑦)
159, 14wi 4 . . . . . 6 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1615, 10, 1wral 2370 . . . . 5 wff 𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1716, 7, 1wral 2370 . . . 4 wff 𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1817, 5, 1wral 2370 . . 3 wff 𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
194, 18wa 103 . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))
203, 19wb 104 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))
Colors of variables: wff set class
This definition is referenced by:  nfso  4153  sopo  4164  soss  4165  soeq1  4166  issod  4170  sowlin  4171  so0  4177  ordsoexmid  4406  soinxp  4537  sosng  4540  cnvsom  5008  isosolem  5641  ltsopr  7252  ltsosr  7407  ltso  7660  xrltso  9365
  Copyright terms: Public domain W3C validator