Definition df-iso 4333

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 4331	. 2 wff R Or A
4	1, 2	wpo 4330	. . 3 wff R Po A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1363	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1363	. . . . . . . 8 class y
9	6, 8, 2	wbr 4034	. . . . . . 7 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1363	. . . . . . . . 9 class z
12	6, 11, 2	wbr 4034	. . . . . . . 8 wff x R z
13	11, 8, 2	wbr 4034	. . . . . . . 8 wff z R y
14	12, 13	wo 709	. . . . . . 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 2475	. . . . 5 wff A. z e. A ( x R y -> ( x R z \/ z R y ) )
17	16, 7, 1	wral 2475	. . . 4 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) )
18	17, 5, 1	wral 2475	. . 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  4338  sopo  4349  soss  4350  soeq1  4351  issod  4355  sowlin  4356  so0  4362  ordsoexmid  4599  soinxp  4734  sosng  4737  cnvsom  5214  isosolem  5874  ltsopr  7682  ltsosr  7850  ltso  8123  xrltso  9890