Definition df-iso 4274

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

This definition is referenced by:  nfso  4279  sopo  4290  soss  4291  soeq1  4292  issod  4296  sowlin  4297  so0  4303  ordsoexmid  4538  soinxp  4673  sosng  4676  cnvsom  5146  isosolem  5791  ltsopr  7533  ltsosr  7701  ltso  7972  xrltso  9728