Definition df-iso 4298

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 4296	. 2 wff R Or A
4	1, 2	wpo 4295	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1352	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1352	. . . . . . . 8 class y
9	6, 8, 2	wbr 4004	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1352	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4004	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4004	. . . . . . . 8 wff z R y
14	12, 13	wo 708	. . . . . . 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 2455	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2455	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2455	. . 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  4303  sopo  4314  soss  4315  soeq1  4316  issod  4320  sowlin  4321  so0  4327  ordsoexmid  4562  soinxp  4697  sosng  4700  cnvsom  5173  isosolem  5825  ltsopr  7595  ltsosr  7763  ltso  8035  xrltso  9796