Definition df-iso 4423

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 4421	. 2 wff R Or A
4	1, 2	wpo 4420	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1397	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1397	. . . . . . . 8 class y
9	6, 8, 2	wbr 4114	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1397	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4114	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4114	. . . . . . . 8 wff z R y
14	12, 13	wo 716	. . . . . . 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 2522	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2522	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2522	. . 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  4428  sopo  4439  soss  4440  soeq1  4441  issod  4445  sowlin  4446  so0  4452  ordsoexmid  4689  soinxp  4825  sosng  4828  cnvsom  5311  isosolem  6003  ltsopr  7927  ltsosr  8095  ltso  8367  xrltso  10148