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

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

Detailed syntax breakdown of Definition df-iso
StepHypRef Expression
1 cA . . 3 class A
2 cR . . 3 class 𝑅
31, 2wor 4022 . 2 wff 𝑅 Or A
41, 2wpo 4021 . . 3 wff 𝑅 Po A
5 vx . . . . . . . . 9 setvar x
65cv 1241 . . . . . . . 8 class x
7 vy . . . . . . . . 9 setvar y
87cv 1241 . . . . . . . 8 class y
96, 8, 2wbr 3754 . . . . . . 7 wff x𝑅y
10 vz . . . . . . . . . 10 setvar z
1110cv 1241 . . . . . . . . 9 class z
126, 11, 2wbr 3754 . . . . . . . 8 wff x𝑅z
1311, 8, 2wbr 3754 . . . . . . . 8 wff z𝑅y
1412, 13wo 628 . . . . . . 7 wff (x𝑅z z𝑅y)
159, 14wi 4 . . . . . 6 wff (x𝑅y → (x𝑅z z𝑅y))
1615, 10, 1wral 2300 . . . . 5 wff z A (x𝑅y → (x𝑅z z𝑅y))
1716, 7, 1wral 2300 . . . 4 wff y A z A (x𝑅y → (x𝑅z z𝑅y))
1817, 5, 1wral 2300 . . 3 wff x A y A z A (x𝑅y → (x𝑅z z𝑅y))
194, 18wa 97 . 2 wff (𝑅 Po A x A y A z A (x𝑅y → (x𝑅z z𝑅y)))
203, 19wb 98 1 wff (𝑅 Or A ↔ (𝑅 Po A x A y A z A (x𝑅y → (x𝑅z z𝑅y))))
Colors of variables: wff set class
This definition is referenced by:  nfso  4029  sopo  4040  soss  4041  soeq1  4042  issod  4046  sowlin  4047  so0  4053  ordsoexmid  4239  soinxp  4352  sosng  4355  cnvsom  4803  isosolem  5404  ltsopr  6560  ltsosr  6644  ltso  6845  xrltso  8435
  Copyright terms: Public domain W3C validator