Definition df-iso 4400

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 4398	. 2 wff 𝑅 Or 𝐴
4	1, 2	wpo 4397	. . 3 wff 𝑅 Po 𝐴
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1397	. . . . . . . 8 class 𝑥
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1397	. . . . . . . 8 class 𝑦
9	6, 8, 2	wbr 4093	. . . . . . 7 wff 𝑥𝑅𝑦
10		vz	. . . . . . . . . 10 setvar 𝑧
11	10	cv 1397	. . . . . . . . 9 class 𝑧
12	6, 11, 2	wbr 4093	. . . . . . . 8 wff 𝑥𝑅𝑧
13	11, 8, 2	wbr 4093	. . . . . . . 8 wff 𝑧𝑅𝑦
14	12, 13	wo 716	. . . . . . 7 wff (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)
15	9, 14	wi 4	. . . . . 6 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
16	15, 10, 1	wral 2511	. . . . 5 wff ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
17	16, 7, 1	wral 2511	. . . 4 wff ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))
18	17, 5, 1	wral 2511	. . 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  4405  sopo  4416  soss  4417  soeq1  4418  issod  4422  sowlin  4423  so0  4429  ordsoexmid  4666  soinxp  4802  sosng  4805  cnvsom  5287  isosolem  5975  ltsopr  7876  ltsosr  8044  ltso  8316  xrltso  10092