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