Definition df-iso 4396

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 4394	. 2 wff R Or A
4	1, 2	wpo 4393	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1396	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1396	. . . . . . . 8 class y
9	6, 8, 2	wbr 4089	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1396	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4089	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4089	. . . . . . . 8 wff z R y
14	12, 13	wo 715	. . . . . . 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 2509	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2509	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2509	. . 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  4401  sopo  4412  soss  4413  soeq1  4414  issod  4418  sowlin  4419  so0  4425  ordsoexmid  4662  soinxp  4798  sosng  4801  cnvsom  5282  isosolem  5970  ltsopr  7821  ltsosr  7989  ltso  8262  xrltso  10036