Definition df-iso 4345

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 4343	. 2 wff R Or A
4	1, 2	wpo 4342	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1372	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1372	. . . . . . . 8 class y
9	6, 8, 2	wbr 4045	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1372	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4045	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4045	. . . . . . . 8 wff z R y
14	12, 13	wo 710	. . . . . . 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 2484	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2484	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2484	. . 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  4350  sopo  4361  soss  4362  soeq1  4363  issod  4367  sowlin  4368  so0  4374  ordsoexmid  4611  soinxp  4746  sosng  4749  cnvsom  5227  isosolem  5895  ltsopr  7711  ltsosr  7879  ltso  8152  xrltso  9920