Definition df-iso 4394

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 4392	. 2 wff R Or A
4	1, 2	wpo 4391	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1396	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1396	. . . . . . . 8 class y
9	6, 8, 2	wbr 4088	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1396	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4088	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4088	. . . . . . . 8 wff z R y
14	12, 13	wo 715	. . . . . . 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 2510	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2510	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2510	. . 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  4399  sopo  4410  soss  4411  soeq1  4412  issod  4416  sowlin  4417  so0  4423  ordsoexmid  4660  soinxp  4796  sosng  4799  cnvsom  5280  isosolem  5964  ltsopr  7815  ltsosr  7983  ltso  8256  xrltso  10030