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

Metamath Proof Explorer

Theorem psslinpr

Description: Proper subset is a linear ordering on positive reals. Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 25-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion psslinpr ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ Q )
2 prub ⊢ ( ( ( 𝐵 ∈ P ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ Q ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑦 <Q 𝑥 ) )
3 1 2 sylan2 ⊢ ( ( ( 𝐵 ∈ P ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑦 <Q 𝑥 ) )
4 prcdnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) )
5 4 adantl ⊢ ( ( ( 𝐵 ∈ P ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) )
6 3 5 syld ⊢ ( ( ( 𝐵 ∈ P ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) )
7 6 exp43 ⊢ ( 𝐵 ∈ P → ( 𝑦 ∈ 𝐵 → ( 𝐴 ∈ P → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) ) ) ) )
8 7 com3r ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ P → ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) ) ) ) )
9 8 imp ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) ) ) )
10 9 imp4a ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑦 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → 𝑦 ∈ 𝐴 ) ) )
11 10 com23 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) ) )
12 11 alrimdv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) ) )
13 12 exlimdv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) ) )
14 nss ⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
15 sspss ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) )
16 14 15 xchnxbi ⊢ ( ¬ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
17 sspss ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) )
18 df-ss ⊢ ( 𝐵 ⊆ 𝐴 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) )
19 17 18 bitr3i ⊢ ( ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) )
20 13 16 19 3imtr4g ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ¬ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) → ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) ) )
21 20 orrd ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) ) )
22 df-3or ⊢ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ 𝐵 ⊊ 𝐴 ) )
23 or32 ⊢ ( ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ 𝐵 ⊊ 𝐴 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
24 orordir ⊢ ( ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ∨ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊊ 𝐴 ∨ 𝐴 = 𝐵 ) ) )
25 eqcom ⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
26 25 orbi2i ⊢ ( ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ( 𝐵 ⊊ 𝐴 ∨ 𝐴 = 𝐵 ) )
27 26 orbi2i ⊢ ( ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊊ 𝐴 ∨ 𝐴 = 𝐵 ) ) )
28 24 27 bitr4i ⊢ ( ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ∨ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) ) )
29 22 23 28 3bitri ⊢ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) ) )
30 21 29 sylibr ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) )