Definition df-iso 4420

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 4418	. 2 wff R Or A
4	1, 2	wpo 4417	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1397	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1397	. . . . . . . 8 class y
9	6, 8, 2	wbr 4111	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1397	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4111	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4111	. . . . . . . 8 wff z R y
14	12, 13	wo 716	. . . . . . 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 2522	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2522	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2522	. . 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 referenced by:  nfso  4425  sopo  4436  soss  4437  soeq1  4438  issod  4442  sowlin  4443  so0  4449  ordsoexmid  4686  soinxp  4822  sosng  4825  cnvsom  5308  isosolem  5999  ltsopr  7913  ltsosr  8081  ltso  8353  xrltso  10132