Definition df-iso 4329

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 4327	. 2 wff R Or A
4	1, 2	wpo 4326	. . 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 4030	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1363	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4030	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4030	. . . . . . . 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 2472	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2472	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2472	. . 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  4334  sopo  4345  soss  4346  soeq1  4347  issod  4351  sowlin  4352  so0  4358  ordsoexmid  4595  soinxp  4730  sosng  4733  cnvsom  5210  isosolem  5868  ltsopr  7658  ltsosr  7826  ltso  8099  xrltso  9865