This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 
 |-