Definition df-iso 4332

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 4330	. 2 wff R Or A
4	1, 2	wpo 4329	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1363	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1363	. . . . . . . 8 class y
9	6, 8, 2	wbr 4033	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1363	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4033	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4033	. . . . . . . 8 wff z R y
14	12, 13	wo 709	. . . . . . 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 2475	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2475	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2475	. . 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  4337  sopo  4348  soss  4349  soeq1  4350  issod  4354  sowlin  4355  so0  4361  ordsoexmid  4598  soinxp  4733  sosng  4736  cnvsom  5213  isosolem  5871  ltsopr  7663  ltsosr  7831  ltso  8104  xrltso  9871