Definition df-iso 4179

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 4177	. 2 wff R Or A
4	1, 2	wpo 4176	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1313	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1313	. . . . . . . 8 class y
9	6, 8, 2	wbr 3895	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1313	. . . . . . . . 9 class z
12	6, 11, 2	wbr 3895	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 3895	. . . . . . . 8 wff z R y
14	12, 13	wo 680	. . . . . . 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 2390	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2390	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2390	. . 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 103	. 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 104	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  4184  sopo  4195  soss  4196  soeq1  4197  issod  4201  sowlin  4202  so0  4208  ordsoexmid  4437  soinxp  4569  sosng  4572  cnvsom  5040  isosolem  5679  ltsopr  7352  ltsosr  7507  ltso  7765  xrltso  9475