Definition df-iso 4061

Description: Define the strict linear order predicate. The expression R Or A is true if relationship R orders A. The property x R y -> ( x R z \/ z R y ) is called weak linearity by Proposition 11.2.3 of [HoTT], p. (varies). If we assumed excluded middle, it would be equivalent to trichotomy, x R y \/ x = y \/ y R x. (Contributed by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)

Assertion

Ref	Expression
df-iso	|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) ) ) )

Distinct variable groups:   x, y, z, R   x, A, y, z

Detailed syntax breakdown of Definition df-iso

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wor 4059	. 2 wff R Or A
4	1, 2	wpo 4058	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1258	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1258	. . . . . . . 8 class y
9	6, 8, 2	wbr 3791	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1258	. . . . . . . . 9 class z
12	6, 11, 2	wbr 3791	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 3791	. . . . . . . 8 wff z R y
14	12, 13	wo 639	. . . . . . 7 wff ( x R z \/ z R y )
15	9, 14	wi 4	. . . . . 6 wff ( x R y -> ( x R z \/ z R y ) )
16	15, 10, 1	wral 2323	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2323	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2323	. . 3 wff A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
19	4, 18	wa 101	. 2 wff ( R Po A /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) ) )
20	3, 19	wb 102	1 wff ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) ) ) )

This definition is referenced by:  nfso  4066  sopo  4077  soss  4078  soeq1  4079  issod  4083  sowlin  4084  so0  4090  ordsoexmid  4313  soinxp  4437  sosng  4440  cnvsom  4888  isosolem  5490  ltsopr  6751  ltsosr  6906  ltso  7154  xrltso  8817