Definition df-iso 4328

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 4326	. 2 wff 𝑅 Or 𝐴
4	1, 2	wpo 4325	. . 3 wff 𝑅 Po 𝐴
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1363	. . . . . . . 8 class 𝑥
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1363	. . . . . . . 8 class 𝑦
9	6, 8, 2	wbr 4029	. . . . . . 7 wff 𝑥𝑅𝑦
10		vz	. . . . . . . . . 10 setvar 𝑧
11	10	cv 1363	. . . . . . . . 9 class 𝑧
12	6, 11, 2	wbr 4029	. . . . . . . 8 wff 𝑥𝑅𝑧
13	11, 8, 2	wbr 4029	. . . . . . . 8 wff 𝑧𝑅𝑦
14	12, 13	wo 709	. . . . . . 7 wff (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)
15	9, 14	wi 4	. . . . . 6 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
16	15, 10, 1	wral 2472	. . . . 5 wff ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
17	16, 7, 1	wral 2472	. . . 4 wff ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
18	17, 5, 1	wral 2472	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
19	4, 18	wa 104	. 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))
20	3, 19	wb 105	1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))))

This definition is referenced by:  nfso  4333  sopo  4344  soss  4345  soeq1  4346  issod  4350  sowlin  4351  so0  4357  ordsoexmid  4594  soinxp  4729  sosng  4732  cnvsom  5209  isosolem  5867  ltsopr  7656  ltsosr  7824  ltso  8097  xrltso  9862