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 e. P. /\ B e. P. ) -> ( A C. B \/ A = B \/ B C. A ) )

Proof

Step Hyp Ref Expression
1 elprnq 
 |-  ( ( A e. P. /\ x e. A ) -> x e. Q. )
2 prub 
 |-  ( ( ( B e. P. /\ y e. B ) /\ x e. Q. ) -> ( -. x e. B -> y
3 1 2 sylan2 
 |-  ( ( ( B e. P. /\ y e. B ) /\ ( A e. P. /\ x e. A ) ) -> ( -. x e. B -> y
4 prcdnq 
 |-  ( ( A e. P. /\ x e. A ) -> ( y  y e. A ) )
5 4 adantl 
 |-  ( ( ( B e. P. /\ y e. B ) /\ ( A e. P. /\ x e. A ) ) -> ( y  y e. A ) )
6 3 5 syld 
 |-  ( ( ( B e. P. /\ y e. B ) /\ ( A e. P. /\ x e. A ) ) -> ( -. x e. B -> y e. A ) )
7 6 exp43 
 |-  ( B e. P. -> ( y e. B -> ( A e. P. -> ( x e. A -> ( -. x e. B -> y e. A ) ) ) ) )
8 7 com3r 
 |-  ( A e. P. -> ( B e. P. -> ( y e. B -> ( x e. A -> ( -. x e. B -> y e. A ) ) ) ) )
9 8 imp 
 |-  ( ( A e. P. /\ B e. P. ) -> ( y e. B -> ( x e. A -> ( -. x e. B -> y e. A ) ) ) )
10 9 imp4a 
 |-  ( ( A e. P. /\ B e. P. ) -> ( y e. B -> ( ( x e. A /\ -. x e. B ) -> y e. A ) ) )
11 10 com23 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( x e. A /\ -. x e. B ) -> ( y e. B -> y e. A ) ) )
12 11 alrimdv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( x e. A /\ -. x e. B ) -> A. y ( y e. B -> y e. A ) ) )
13 12 exlimdv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. x ( x e. A /\ -. x e. B ) -> A. y ( y e. B -> y e. A ) ) )
14 nss 
 |-  ( -. A C_ B <-> E. x ( x e. A /\ -. x e. B ) )
15 sspss 
 |-  ( A C_ B <-> ( A C. B \/ A = B ) )
16 14 15 xchnxbi 
 |-  ( -. ( A C. B \/ A = B ) <-> E. x ( x e. A /\ -. x e. B ) )
17 sspss 
 |-  ( B C_ A <-> ( B C. A \/ B = A ) )
18 dfss2 
 |-  ( B C_ A <-> A. y ( y e. B -> y e. A ) )
19 17 18 bitr3i 
 |-  ( ( B C. A \/ B = A ) <-> A. y ( y e. B -> y e. A ) )
20 13 16 19 3imtr4g 
 |-  ( ( A e. P. /\ B e. P. ) -> ( -. ( A C. B \/ A = B ) -> ( B C. A \/ B = A ) ) )
21 20 orrd 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( A C. B \/ A = B ) \/ ( B C. A \/ B = A ) ) )
22 df-3or 
 |-  ( ( A C. B \/ A = B \/ B C. A ) <-> ( ( A C. B \/ A = B ) \/ B C. A ) )
23 or32 
 |-  ( ( ( A C. B \/ A = B ) \/ B C. A ) <-> ( ( A C. B \/ B C. A ) \/ A = B ) )
24 orordir 
 |-  ( ( ( A C. B \/ B C. A ) \/ A = B ) <-> ( ( A C. B \/ A = B ) \/ ( B C. A \/ A = B ) ) )
25 eqcom 
 |-  ( B = A <-> A = B )
26 25 orbi2i 
 |-  ( ( B C. A \/ B = A ) <-> ( B C. A \/ A = B ) )
27 26 orbi2i 
 |-  ( ( ( A C. B \/ A = B ) \/ ( B C. A \/ B = A ) ) <-> ( ( A C. B \/ A = B ) \/ ( B C. A \/ A = B ) ) )
28 24 27 bitr4i 
 |-  ( ( ( A C. B \/ B C. A ) \/ A = B ) <-> ( ( A C. B \/ A = B ) \/ ( B C. A \/ B = A ) ) )
29 22 23 28 3bitri 
 |-  ( ( A C. B \/ A = B \/ B C. A ) <-> ( ( A C. B \/ A = B ) \/ ( B C. A \/ B = A ) ) )
30 21 29 sylibr 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A C. B \/ A = B \/ B C. A ) )