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 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⊂ B ∨ A = B ∨ B ⊂ A

Proof

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