Definition df-iso 4392

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 4390	. 2 wff R Or A
4	1, 2	wpo 4389	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1394	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1394	. . . . . . . 8 class y
9	6, 8, 2	wbr 4086	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1394	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4086	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4086	. . . . . . . 8 wff z R y
14	12, 13	wo 713	. . . . . . 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 2508	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2508	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2508	. . 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  4397  sopo  4408  soss  4409  soeq1  4410  issod  4414  sowlin  4415  so0  4421  ordsoexmid  4658  soinxp  4794  sosng  4797  cnvsom  5278  isosolem  5960  ltsopr  7806  ltsosr  7974  ltso  8247  xrltso  10021