Definition df-iso 4297

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 4295	. 2 wff R Or A
4	1, 2	wpo 4294	. . 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 4003	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1352	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4003	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4003	. . . . . . . 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  4302  sopo  4313  soss  4314  soeq1  4315  issod  4319  sowlin  4320  so0  4326  ordsoexmid  4561  soinxp  4696  sosng  4699  cnvsom  5172  isosolem  5824  ltsopr  7594  ltsosr  7762  ltso  8034  xrltso  9795