Definition df-iso 4031

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 4029	. 2 wff R Or A
4	1, 2	wpo 4028	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1242	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1242	. . . . . . . 8 class y
9	6, 8, 2	wbr 3761	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1242	. . . . . . . . 9 class z
12	6, 11, 2	wbr 3761	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 3761	. . . . . . . 8 wff z R y
14	12, 13	wo 629	. . . . . . 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 2303	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2303	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2303	. . 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 97	. 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 98	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  4036  sopo  4047  soss  4048  soeq1  4049  issod  4053  sowlin  4054  so0  4060  ordsoexmid  4271  soinxp  4388  sosng  4391  cnvsom  4839  isosolem  5441  ltsopr  6666  ltsosr  6821  ltso  7067  xrltso  8675