Definition df-iso 4282

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 4280	. 2 wff R Or A
4	1, 2	wpo 4279	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1347	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1347	. . . . . . . 8 class y
9	6, 8, 2	wbr 3989	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1347	. . . . . . . . 9 class z
12	6, 11, 2	wbr 3989	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 3989	. . . . . . . 8 wff z R y
14	12, 13	wo 703	. . . . . . 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 2448	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2448	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2448	. . 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 103	. 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 104	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  4287  sopo  4298  soss  4299  soeq1  4300  issod  4304  sowlin  4305  so0  4311  ordsoexmid  4546  soinxp  4681  sosng  4684  cnvsom  5154  isosolem  5803  ltsopr  7558  ltsosr  7726  ltso  7997  xrltso  9753