Definition df-iso 4034

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wor 4032	. 2 wff 𝑅 Or 𝐴
4	1, 2	wpo 4031	. . 3 wff 𝑅 Po 𝐴
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1242	. . . . . . . 8 class 𝑥
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1242	. . . . . . . 8 class 𝑦
9	6, 8, 2	wbr 3764	. . . . . . 7 wff 𝑥𝑅𝑦
10		vz	. . . . . . . . . 10 setvar 𝑧
11	10	cv 1242	. . . . . . . . 9 class 𝑧
12	6, 11, 2	wbr 3764	. . . . . . . 8 wff 𝑥𝑅𝑧
13	11, 8, 2	wbr 3764	. . . . . . . 8 wff 𝑧𝑅𝑦
14	12, 13	wo 629	. . . . . . 7 wff (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)
15	9, 14	wi 4	. . . . . 6 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
16	15, 10, 1	wral 2306	. . . . 5 wff ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
17	16, 7, 1	wral 2306	. . . 4 wff ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
18	17, 5, 1	wral 2306	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
19	4, 18	wa 97	. 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))
20	3, 19	wb 98	1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))))

This definition is referenced by:  nfso  4039  sopo  4050  soss  4051  soeq1  4052  issod  4056  sowlin  4057  so0  4063  ordsoexmid  4286  soinxp  4410  sosng  4413  cnvsom  4861  isosolem  5463  ltsopr  6694  ltsosr  6849  ltso  7096  xrltso  8717