Definition df-iso 4219

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 4217	. 2 wff R Or A
4	1, 2	wpo 4216	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1330	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1330	. . . . . . . 8 class y
9	6, 8, 2	wbr 3929	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1330	. . . . . . . . 9 class z
12	6, 11, 2	wbr 3929	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 3929	. . . . . . . 8 wff z R y
14	12, 13	wo 697	. . . . . . 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 2416	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2416	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2416	. . 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 103	. 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 104	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  4224  sopo  4235  soss  4236  soeq1  4237  issod  4241  sowlin  4242  so0  4248  ordsoexmid  4477  soinxp  4609  sosng  4612  cnvsom  5082  isosolem  5725  ltsopr  7404  ltsosr  7572  ltso  7842  xrltso  9582