Theorem ltsopr

Description: Positive real 'less than' is a strict ordering. Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 25-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	ltsopr	|-

Proof

Step	Hyp	Ref	Expression
1		pssirr	|- -. x C. x
2		ltprord	|- ( ( x e. P. /\ x e. P. ) -> ( x x C. x ) )
3	1 2	mtbiri	|- ( ( x e. P. /\ x e. P. ) -> -. x
4	3	anidms	|- ( x e. P. -> -. x
5		psstr	|- ( ( x C. y /\ y C. z ) -> x C. z )
6		ltprord	|- ( ( x e. P. /\ y e. P. ) -> ( x x C. y ) )
7	6	3adant3	|- ( ( x e. P. /\ y e. P. /\ z e. P. ) -> ( x x C. y ) )
8		ltprord	|- ( ( y e. P. /\ z e. P. ) -> ( y y C. z ) )
9	8	3adant1	|- ( ( x e. P. /\ y e. P. /\ z e. P. ) -> ( y y C. z ) )
10	7 9	anbi12d	|- ( ( x e. P. /\ y e. P. /\ z e. P. ) -> ( ( x ( x C. y /\ y C. z ) ) )
11		ltprord	|- ( ( x e. P. /\ z e. P. ) -> ( x x C. z ) )
12	11	3adant2	|- ( ( x e. P. /\ y e. P. /\ z e. P. ) -> ( x x C. z ) )
13	10 12	imbi12d	|- ( ( x e. P. /\ y e. P. /\ z e. P. ) -> ( ( ( x x ( ( x C. y /\ y C. z ) -> x C. z ) ) )
14	5 13	mpbiri	|- ( ( x e. P. /\ y e. P. /\ z e. P. ) -> ( ( x x
15		psslinpr	|- ( ( x e. P. /\ y e. P. ) -> ( x C. y \/ x = y \/ y C. x ) )
16		biidd	|- ( ( x e. P. /\ y e. P. ) -> ( x = y <-> x = y ) )
17		ltprord	|- ( ( y e. P. /\ x e. P. ) -> ( y y C. x ) )
18	17	ancoms	|- ( ( x e. P. /\ y e. P. ) -> ( y y C. x ) )
19	6 16 18	3orbi123d	|- ( ( x e. P. /\ y e. P. ) -> ( ( x ( x C. y \/ x = y \/ y C. x ) ) )
20	15 19	mpbird	|- ( ( x e. P. /\ y e. P. ) -> ( x
21	4 14 20	issoi	|-