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 ⊢ ¬ x ⊂ x
2 ltprord ⊢ x ∈ 𝑷 ∧ x ∈ 𝑷 → x < 𝑷 x ↔ x ⊂ x
3 1 2 mtbiri ⊢ x ∈ 𝑷 ∧ x ∈ 𝑷 → ¬ x < 𝑷 x
4 3 anidms ⊢ x ∈ 𝑷 → ¬ x < 𝑷 x
5 psstr ⊢ x ⊂ y ∧ y ⊂ z → x ⊂ z
6 ltprord ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 → x < 𝑷 y ↔ x ⊂ y
7 6 3adant3 ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 → x < 𝑷 y ↔ x ⊂ y
8 ltprord ⊢ y ∈ 𝑷 ∧ z ∈ 𝑷 → y < 𝑷 z ↔ y ⊂ z
9 8 3adant1 ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 → y < 𝑷 z ↔ y ⊂ z
10 7 9 anbi12d ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 → x < 𝑷 y ∧ y < 𝑷 z ↔ x ⊂ y ∧ y ⊂ z
11 ltprord ⊢ x ∈ 𝑷 ∧ z ∈ 𝑷 → x < 𝑷 z ↔ x ⊂ z
12 11 3adant2 ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 → x < 𝑷 z ↔ x ⊂ z
13 10 12 imbi12d ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 → x < 𝑷 y ∧ y < 𝑷 z → x < 𝑷 z ↔ x ⊂ y ∧ y ⊂ z → x ⊂ z
14 5 13 mpbiri ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 → x < 𝑷 y ∧ y < 𝑷 z → x < 𝑷 z
15 psslinpr ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 → x ⊂ y ∨ x = y ∨ y ⊂ x
16 biidd ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 → x = y ↔ x = y
17 ltprord ⊢ y ∈ 𝑷 ∧ x ∈ 𝑷 → y < 𝑷 x ↔ y ⊂ x
18 17 ancoms ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 → y < 𝑷 x ↔ y ⊂ x
19 6 16 18 3orbi123d ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 → x < 𝑷 y ∨ x = y ∨ y < 𝑷 x ↔ x ⊂ y ∨ x = y ∨ y ⊂ x
20 15 19 mpbird ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 → x < 𝑷 y ∨ x = y ∨ y < 𝑷 x
21 4 14 20 issoi ⊢ < 𝑷 Or 𝑷