Definition df-iso 4362

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 4360	. 2 wff R Or A
4	1, 2	wpo 4359	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1372	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1372	. . . . . . . 8 class y
9	6, 8, 2	wbr 4059	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1372	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4059	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4059	. . . . . . . 8 wff z R y
14	12, 13	wo 710	. . . . . . 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 2486	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2486	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2486	. . 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  4367  sopo  4378  soss  4379  soeq1  4380  issod  4384  sowlin  4385  so0  4391  ordsoexmid  4628  soinxp  4763  sosng  4766  cnvsom  5245  isosolem  5916  ltsopr  7744  ltsosr  7912  ltso  8185  xrltso  9953