Definition df-iso 4299

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 4297	. 2 wff R Or A
4	1, 2	wpo 4296	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1352	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1352	. . . . . . . 8 class y
9	6, 8, 2	wbr 4005	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1352	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4005	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4005	. . . . . . . 8 wff z R y
14	12, 13	wo 708	. . . . . . 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 2455	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2455	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2455	. . 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  4304  sopo  4315  soss  4316  soeq1  4317  issod  4321  sowlin  4322  so0  4328  ordsoexmid  4563  soinxp  4698  sosng  4701  cnvsom  5174  isosolem  5828  ltsopr  7598  ltsosr  7766  ltso  8038  xrltso  9799