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	syl5bi	|- ( 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	syl6bi	|- ( ( 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	syl5bi	|- ( 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. )