Metamath Proof Explorer

Theorem suplem1pr

Description: The union of a nonempty, bounded set of positive reals is a positive real. Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion suplem1pr 
|- ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 U. A e. P. )

Proof

Step Hyp Ref Expression
1 ltrelpr 
 |-
2 1 brel 
 |-  ( y 
 ( y e. P. /\ x e. P. ) )
3 2 simpld 
 |-  ( y 
 y e. P. )
4 3 ralimi 
 |-  ( A. y e. A y 
 A. y e. A y e. P. )
5 dfss3 
 |-  ( A C_ P. <-> A. y e. A y e. P. )
6 4 5 sylibr 
 |-  ( A. y e. A y 
 A C_ P. )
7 6 rexlimivw 
 |-  ( E. x e. P. A. y e. A y 
 A C_ P. )
8 7 adantl 
 |-  ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 A C_ P. )
9 n0 
 |-  ( A =/= (/) <-> E. z z e. A )
10 ssel 
 |-  ( A C_ P. -> ( z e. A -> z e. P. ) )
11 prn0 
 |-  ( z e. P. -> z =/= (/) )
12 0pss 
 |-  ( (/) C. z <-> z =/= (/) )
13 11 12 sylibr 
 |-  ( z e. P. -> (/) C. z )
14 elssuni 
 |-  ( z e. A -> z C_ U. A )
15 psssstr 
 |-  ( ( (/) C. z /\ z C_ U. A ) -> (/) C. U. A )
16 13 14 15 syl2an 
 |-  ( ( z e. P. /\ z e. A ) -> (/) C. U. A )
17 16 expcom 
 |-  ( z e. A -> ( z e. P. -> (/) C. U. A ) )
18 10 17 sylcom 
 |-  ( A C_ P. -> ( z e. A -> (/) C. U. A ) )
19 18 exlimdv 
 |-  ( A C_ P. -> ( E. z z e. A -> (/) C. U. A ) )
20 9 19 biimtrid 
 |-  ( A C_ P. -> ( A =/= (/) -> (/) C. U. A ) )
21 prpssnq 
 |-  ( x e. P. -> x C. Q. )
22 21 adantl 
 |-  ( ( A C_ P. /\ x e. P. ) -> x C. Q. )
23 ltprord 
 |-  ( ( y e. P. /\ x e. P. ) -> ( y 
 y C. x ) )
24 pssss 
 |-  ( y C. x -> y C_ x )
25 23 24 biimtrdi 
 |-  ( ( y e. P. /\ x e. P. ) -> ( y 
 y C_ x ) )
26 2 25 mpcom 
 |-  ( y 
 y C_ x )
27 26 ralimi 
 |-  ( A. y e. A y 
 A. y e. A y C_ x )
28 unissb 
 |-  ( U. A C_ x <-> A. y e. A y C_ x )
29 27 28 sylibr 
 |-  ( A. y e. A y 
 U. A C_ x )
30 sspsstr 
 |-  ( ( U. A C_ x /\ x C. Q. ) -> U. A C. Q. )
31 30 expcom 
 |-  ( x C. Q. -> ( U. A C_ x -> U. A C. Q. ) )
32 22 29 31 syl2im 
 |-  ( ( A C_ P. /\ x e. P. ) -> ( A. y e. A y 
 U. A C. Q. ) )
33 32 rexlimdva 
 |-  ( A C_ P. -> ( E. x e. P. A. y e. A y 
 U. A C. Q. ) )
34 20 33 anim12d 
 |-  ( A C_ P. -> ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 ( (/) C. U. A /\ U. A C. Q. ) ) )
35 8 34 mpcom 
 |-  ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 ( (/) C. U. A /\ U. A C. Q. ) )
36 prcdnq 
 |-  ( ( z e. P. /\ x e. z ) -> ( y  y e. z ) )
37 36 ex 
 |-  ( z e. P. -> ( x e. z -> ( y  y e. z ) ) )
38 37 com3r 
 |-  ( y  ( z e. P. -> ( x e. z -> y e. z ) ) )
39 10 38 sylan9 
 |-  ( ( A C_ P. /\ y  ( z e. A -> ( x e. z -> y e. z ) ) )
40 39 reximdvai 
 |-  ( ( A C_ P. /\ y  ( E. z e. A x e. z -> E. z e. A y e. z ) )
41 eluni2 
 |-  ( x e. U. A <-> E. z e. A x e. z )
42 eluni2 
 |-  ( y e. U. A <-> E. z e. A y e. z )
43 40 41 42 3imtr4g 
 |-  ( ( A C_ P. /\ y  ( x e. U. A -> y e. U. A ) )
44 43 ex 
 |-  ( A C_ P. -> ( y  ( x e. U. A -> y e. U. A ) ) )
45 44 com23 
 |-  ( A C_ P. -> ( x e. U. A -> ( y  y e. U. A ) ) )
46 45 alrimdv 
 |-  ( A C_ P. -> ( x e. U. A -> A. y ( y  y e. U. A ) ) )
47 eluni 
 |-  ( x e. U. A <-> E. z ( x e. z /\ z e. A ) )
48 prnmax 
 |-  ( ( z e. P. /\ x e. z ) -> E. y e. z x
49 48 ex 
 |-  ( z e. P. -> ( x e. z -> E. y e. z x
50 10 49 syl6 
 |-  ( A C_ P. -> ( z e. A -> ( x e. z -> E. y e. z x
51 50 com23 
 |-  ( A C_ P. -> ( x e. z -> ( z e. A -> E. y e. z x
52 51 imp 
 |-  ( ( A C_ P. /\ x e. z ) -> ( z e. A -> E. y e. z x
53 ssrexv 
 |-  ( z C_ U. A -> ( E. y e. z x  E. y e. U. A x
54 14 53 syl 
 |-  ( z e. A -> ( E. y e. z x  E. y e. U. A x
55 52 54 sylcom 
 |-  ( ( A C_ P. /\ x e. z ) -> ( z e. A -> E. y e. U. A x
56 55 expimpd 
 |-  ( A C_ P. -> ( ( x e. z /\ z e. A ) -> E. y e. U. A x
57 56 exlimdv 
 |-  ( A C_ P. -> ( E. z ( x e. z /\ z e. A ) -> E. y e. U. A x
58 47 57 biimtrid 
 |-  ( A C_ P. -> ( x e. U. A -> E. y e. U. A x
59 46 58 jcad 
 |-  ( A C_ P. -> ( x e. U. A -> ( A. y ( y  y e. U. A ) /\ E. y e. U. A x
60 59 ralrimiv 
 |-  ( A C_ P. -> A. x e. U. A ( A. y ( y  y e. U. A ) /\ E. y e. U. A x
61 8 60 syl 
 |-  ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 A. x e. U. A ( A. y ( y  y e. U. A ) /\ E. y e. U. A x
62 elnp 
 |-  ( U. A e. P. <-> ( ( (/) C. U. A /\ U. A C. Q. ) /\ A. x e. U. A ( A. y ( y  y e. U. A ) /\ E. y e. U. A x
63 35 61 62 sylanbrc 
 |-  ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 U. A e. P. )