Definition df-iso 4052

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 4050	. 2 wff 𝑅 Or 𝐴
4	1, 2	wpo 4049	. . 3 wff 𝑅 Po 𝐴
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1283	. . . . . . . 8 class 𝑥
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1283	. . . . . . . 8 class 𝑦
9	6, 8, 2	wbr 3785	. . . . . . 7 wff 𝑥𝑅𝑦
10		vz	. . . . . . . . . 10 setvar 𝑧
11	10	cv 1283	. . . . . . . . 9 class 𝑧
12	6, 11, 2	wbr 3785	. . . . . . . 8 wff 𝑥𝑅𝑧
13	11, 8, 2	wbr 3785	. . . . . . . 8 wff 𝑧𝑅𝑦
14	12, 13	wo 661	. . . . . . 7 wff (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)
15	9, 14	wi 4	. . . . . 6 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
16	15, 10, 1	wral 2348	. . . . 5 wff ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
17	16, 7, 1	wral 2348	. . . 4 wff ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
18	17, 5, 1	wral 2348	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
19	4, 18	wa 102	. 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))
20	3, 19	wb 103	1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))))

This definition is referenced by:  nfso  4057  sopo  4068  soss  4069  soeq1  4070  issod  4074  sowlin  4075  so0  4081  ordsoexmid  4305  soinxp  4428  sosng  4431  cnvsom  4881  isosolem  5483  ltsopr  6786  ltsosr  6941  ltso  7189  xrltso  8871