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

Proof

Step Hyp Ref Expression
1 pssirr ⊢ ¬ 𝑥 ⊊ 𝑥
2 ltprord ⊢ ( ( 𝑥 ∈ P ∧ 𝑥 ∈ P ) → ( 𝑥 <P 𝑥 ↔ 𝑥 ⊊ 𝑥 ) )
3 1 2 mtbiri ⊢ ( ( 𝑥 ∈ P ∧ 𝑥 ∈ P ) → ¬ 𝑥 <P 𝑥 )
4 3 anidms ⊢ ( 𝑥 ∈ P → ¬ 𝑥 <P 𝑥 )
5 psstr ⊢ ( ( 𝑥 ⊊ 𝑦 ∧ 𝑦 ⊊ 𝑧 ) → 𝑥 ⊊ 𝑧 )
6 ltprord ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( 𝑥 <P 𝑦 ↔ 𝑥 ⊊ 𝑦 ) )
7 6 3adant3 ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 <P 𝑦 ↔ 𝑥 ⊊ 𝑦 ) )
8 ltprord ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑦 <P 𝑧 ↔ 𝑦 ⊊ 𝑧 ) )
9 8 3adant1 ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑦 <P 𝑧 ↔ 𝑦 ⊊ 𝑧 ) )
10 7 9 anbi12d ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ( 𝑥 <P 𝑦 ∧ 𝑦 <P 𝑧 ) ↔ ( 𝑥 ⊊ 𝑦 ∧ 𝑦 ⊊ 𝑧 ) ) )
11 ltprord ⊢ ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 <P 𝑧 ↔ 𝑥 ⊊ 𝑧 ) )
12 11 3adant2 ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 <P 𝑧 ↔ 𝑥 ⊊ 𝑧 ) )
13 10 12 imbi12d ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ( ( 𝑥 <P 𝑦 ∧ 𝑦 <P 𝑧 ) → 𝑥 <P 𝑧 ) ↔ ( ( 𝑥 ⊊ 𝑦 ∧ 𝑦 ⊊ 𝑧 ) → 𝑥 ⊊ 𝑧 ) ) )
14 5 13 mpbiri ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ( 𝑥 <P 𝑦 ∧ 𝑦 <P 𝑧 ) → 𝑥 <P 𝑧 ) )
15 psslinpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( 𝑥 ⊊ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ⊊ 𝑥 ) )
16 biidd ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 ) )
17 ltprord ⊢ ( ( 𝑦 ∈ P ∧ 𝑥 ∈ P ) → ( 𝑦 <P 𝑥 ↔ 𝑦 ⊊ 𝑥 ) )
18 17 ancoms ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( 𝑦 <P 𝑥 ↔ 𝑦 ⊊ 𝑥 ) )
19 6 16 18 3orbi123d ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑥 <P 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 <P 𝑥 ) ↔ ( 𝑥 ⊊ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ⊊ 𝑥 ) ) )
20 15 19 mpbird ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( 𝑥 <P 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 <P 𝑥 ) )
21 4 14 20 issoi ⊢ <P Or P