Definition df-iso 4388

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 4386	. 2 wff R Or A
4	1, 2	wpo 4385	. . 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 4083	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1394	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4083	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4083	. . . . . . . 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  4393  sopo  4404  soss  4405  soeq1  4406  issod  4410  sowlin  4411  so0  4417  ordsoexmid  4654  soinxp  4789  sosng  4792  cnvsom  5272  isosolem  5954  ltsopr  7794  ltsosr  7962  ltso  8235  xrltso  10004