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

Definition df-iso 4312
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 4310 . 2 wff 𝑅 Or 𝐴
41, 2wpo 4309 . . 3 wff 𝑅 Po 𝐴
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1363 . . . . . . . 8 class 𝑥
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1363 . . . . . . . 8 class 𝑦
96, 8, 2wbr 4018 . . . . . . 7 wff 𝑥𝑅𝑦
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1363 . . . . . . . . 9 class 𝑧
126, 11, 2wbr 4018 . . . . . . . 8 wff 𝑥𝑅𝑧
1311, 8, 2wbr 4018 . . . . . . . 8 wff 𝑧𝑅𝑦
1412, 13wo 709 . . . . . . 7 wff (𝑥𝑅𝑧𝑧𝑅𝑦)
159, 14wi 4 . . . . . 6 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1615, 10, 1wral 2468 . . . . 5 wff 𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1716, 7, 1wral 2468 . . . 4 wff 𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
1817, 5, 1wral 2468 . . 3 wff 𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))
194, 18wa 104 . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))
203, 19wb 105 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))
Colors of variables: wff set class
This definition is referenced by:  nfso  4317  sopo  4328  soss  4329  soeq1  4330  issod  4334  sowlin  4335  so0  4341  ordsoexmid  4576  soinxp  4711  sosng  4714  cnvsom  5187  isosolem  5841  ltsopr  7613  ltsosr  7781  ltso  8053  xrltso  9814
  Copyright terms: Public domain W3C validator