Definition df-iso 4442

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 4440	. 2 wff R Or A
4	1, 2	wpo 4439	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1401	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1401	. . . . . . . 8 class y
9	6, 8, 2	wbr 4130	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1401	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4130	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4130	. . . . . . . 8 wff z R y
14	12, 13	wo 720	. . . . . . 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 2528	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2528	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2528	. . 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 used by:  nfso  4447  sopo  4458  soss  4459  soeq1  4460  issod  4464  sowlin  4465  so0  4471  ordsoexmid  4709  soinxp  4845  sosng  4848  cnvsom  5331  isosolem  6030  ltsopr  7963  ltsosr  8131  ltso  8403  xrltso  10198