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

Definition df-iso 4031
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 4029 . 2 wff 𝑅 Or 𝐴
41, 2wpo 4028 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1242 . . . . . . . 8 class 𝑥
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1242 . . . . . . . 8 class 𝑦
96, 8, 2wbr 3761 . . . . . . 7 wff 𝑥𝑅𝑦
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1242 . . . . . . . . 9 class 𝑧
126, 11, 2wbr 3761 . . . . . . . 8 wff 𝑥𝑅𝑧
1311, 8, 2wbr 3761 . . . . . . . 8 wff 𝑧𝑅𝑦
1412, 13wo 629 . . . . . . 7 wff (𝑥𝑅𝑧𝑧𝑅𝑦)
159, 14wi 4 . . . . . 6 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1615, 10, 1wral 2303 . . . . 5 wff 𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1716, 7, 1wral 2303 . . . 4 wff 𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1817, 5, 1wral 2303 . . 3 wff 𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
194, 18wa 97 . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))
203, 19wb 98 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))
Colors of variables: wff set class
This definition is referenced by:  nfso  4036  sopo  4047  soss  4048  soeq1  4049  issod  4053  sowlin  4054  so0  4060  ordsoexmid  4271  soinxp  4388  sosng  4391  cnvsom  4839  isosolem  5441  ltsopr  6666  ltsosr  6821  ltso  7067  xrltso  8675
  Copyright terms: Public domain W3C validator