Definition df-iso 4025

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 4023	. 2 wff 𝑅 Or A
4	1, 2	wpo 4022	. . 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 3755	. . . . . . 7 wff x𝑅y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1241	. . . . . . . . 9 class z
12	6, 11, 2	wbr 3755	. . . . . . . 8 wff x𝑅z
13	11, 8, 2	wbr 3755	. . . . . . . 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  4030  sopo  4041  soss  4042  soeq1  4043  issod  4047  sowlin  4048  so0  4054  ordsoexmid  4240  soinxp  4353  sosng  4356  cnvsom  4804  isosolem  5406  ltsopr  6570  ltsosr  6692  ltso  6893  xrltso  8487