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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class 𝑅
3	1, 2	wor 4022	. 2 wff 𝑅 Or A
4	1, 2	wpo 4021	. . 3 wff 𝑅 Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1241	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1241	. . . . . . . 8 class y
9	6, 8, 2	wbr 3754	. . . . . . 7 wff x𝑅y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1241	. . . . . . . . 9 class z
12	6, 11, 2	wbr 3754	. . . . . . . 8 wff x𝑅z
13	11, 8, 2	wbr 3754	. . . . . . . 8 wff z𝑅y
14	12, 13	wo 628	. . . . . . 7 wff (x𝑅z ∨ z𝑅y)
15	9, 14	wi 4	. . . . . 6 wff (x𝑅y → (x𝑅z ∨ z𝑅y))
16	15, 10, 1	wral 2300	. . . . 5 wff ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y))
17	16, 7, 1	wral 2300	. . . 4 wff ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y))
18	17, 5, 1	wral 2300	. . 3 wff ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y))
19	4, 18	wa 97	. 2 wff (𝑅 Po A ∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y)))
20	3, 19	wb 98	1 wff (𝑅 Or A ↔ (𝑅 Po A ∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y))))

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