Definition df-iso 4052

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 4050	. 2 wff R Or A
4	1, 2	wpo 4049	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1283	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1283	. . . . . . . 8 class y
9	6, 8, 2	wbr 3785	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1283	. . . . . . . . 9 class z
12	6, 11, 2	wbr 3785	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 3785	. . . . . . . 8 wff z R y
14	12, 13	wo 661	. . . . . . 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 2348	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2348	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2348	. . 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 102	. 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 103	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  4057  sopo  4068  soss  4069  soeq1  4070  issod  4074  sowlin  4075  so0  4081  ordsoexmid  4305  soinxp  4428  sosng  4431  cnvsom  4881  isosolem  5483  ltsopr  6786  ltsosr  6941  ltso  7189  xrltso  8871