Definition df-iso 4444

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 4442	. 2 wff R Or A
4	1, 2	wpo 4441	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1401	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1401	. . . . . . . 8 class y
9	6, 8, 2	wbr 4131	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1401	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4131	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4131	. . . . . . . 8 wff z R y
14	12, 13	wo 720	. . . . . . 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 2528	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2528	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2528	. . 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 104	. 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 105	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 used by:  nfso  4449  sopo  4460  soss  4461  soeq1  4462  issod  4466  sowlin  4467  so0  4473  ordsoexmid  4711  soinxp  4847  sosng  4850  cnvsom  5334  isosolem  6033  ltsopr  7969  ltsosr  8137  ltso  8409  xrltso  10215