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→∀yy∈B→y∈A
13 12 exlimdv ⊢A∈𝑷∧B∈𝑷→∃xx∈A∧¬x∈B→∀yy∈B→y∈A
14 nss ⊢¬A⊆B↔∃xx∈A∧¬x∈B
15 sspss ⊢A⊆B↔A⊂B∨A=B
16 14 15 xchnxbi ⊢¬A⊂B∨A=B↔∃xx∈A∧¬x∈B
17 sspss ⊢B⊆A↔B⊂A∨B=A
18 df-ss ⊢B⊆A↔∀yy∈B→y∈A
19 17 18 bitr3i ⊢B⊂A∨B=A↔∀yy∈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