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

Definition df-iso 4189
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 4187 . 2 wff 𝑅 Or 𝐴
41, 2wpo 4186 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1315 . . . . . . . 8 class 𝑥
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1315 . . . . . . . 8 class 𝑦
96, 8, 2wbr 3899 . . . . . . 7 wff 𝑥𝑅𝑦
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1315 . . . . . . . . 9 class 𝑧
126, 11, 2wbr 3899 . . . . . . . 8 wff 𝑥𝑅𝑧
1311, 8, 2wbr 3899 . . . . . . . 8 wff 𝑧𝑅𝑦
1412, 13wo 682 . . . . . . 7 wff (𝑥𝑅𝑧𝑧𝑅𝑦)
159, 14wi 4 . . . . . 6 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1615, 10, 1wral 2393 . . . . 5 wff 𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1716, 7, 1wral 2393 . . . 4 wff 𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1817, 5, 1wral 2393 . . 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  4194  sopo  4205  soss  4206  soeq1  4207  issod  4211  sowlin  4212  so0  4218  ordsoexmid  4447  soinxp  4579  sosng  4582  cnvsom  5052  isosolem  5693  ltsopr  7372  ltsosr  7540  ltso  7810  xrltso  9537
  Copyright terms: Public domain W3C validator