Definition df-iso 4252

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 4250	. 2 wff R Or A
4	1, 2	wpo 4249	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1331	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1331	. . . . . . . 8 class y
9	6, 8, 2	wbr 3961	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1331	. . . . . . . . 9 class z
12	6, 11, 2	wbr 3961	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 3961	. . . . . . . 8 wff z R y
14	12, 13	wo 698	. . . . . . 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 2432	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2432	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2432	. . 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  4257  sopo  4268  soss  4269  soeq1  4270  issod  4274  sowlin  4275  so0  4281  ordsoexmid  4515  soinxp  4649  sosng  4652  cnvsom  5122  isosolem  5765  ltsopr  7495  ltsosr  7663  ltso  7934  xrltso  9681