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

Proof

Step Hyp Ref Expression
1 pssirr ¬xx
2 ltprord x𝑷x𝑷x<𝑷xxx
3 1 2 mtbiri x𝑷x𝑷¬x<𝑷x
4 3 anidms x𝑷¬x<𝑷x
5 psstr xyyzxz
6 ltprord x𝑷y𝑷x<𝑷yxy
7 6 3adant3 x𝑷y𝑷z𝑷x<𝑷yxy
8 ltprord y𝑷z𝑷y<𝑷zyz
9 8 3adant1 x𝑷y𝑷z𝑷y<𝑷zyz
10 7 9 anbi12d x𝑷y𝑷z𝑷x<𝑷yy<𝑷zxyyz
11 ltprord x𝑷z𝑷x<𝑷zxz
12 11 3adant2 x𝑷y𝑷z𝑷x<𝑷zxz
13 10 12 imbi12d x𝑷y𝑷z𝑷x<𝑷yy<𝑷zx<𝑷zxyyzxz
14 5 13 mpbiri x𝑷y𝑷z𝑷x<𝑷yy<𝑷zx<𝑷z
15 psslinpr x𝑷y𝑷xyx=yyx
16 biidd x𝑷y𝑷x=yx=y
17 ltprord y𝑷x𝑷y<𝑷xyx
18 17 ancoms x𝑷y𝑷y<𝑷xyx
19 6 16 18 3orbi123d x𝑷y𝑷x<𝑷yx=yy<𝑷xxyx=yyx
20 15 19 mpbird x𝑷y𝑷x<𝑷yx=yy<𝑷x
21 4 14 20 issoi <𝑷Or𝑷