Definition df-iso 4440

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 4438	. 2 wff R Or A
4	1, 2	wpo 4437	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1401	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1401	. . . . . . . 8 class y
9	6, 8, 2	wbr 4128	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1401	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4128	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4128	. . . . . . . 8 wff z R y
14	12, 13	wo 720	. . . . . . 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 2528	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2528	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2528	. . 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  4445  sopo  4456  soss  4457  soeq1  4458  issod  4462  sowlin  4463  so0  4469  ordsoexmid  4707  soinxp  4843  sosng  4846  cnvsom  5329  isosolem  6023  ltsopr  7956  ltsosr  8124  ltso  8396  xrltso  10180