Theorem suplem2pr

Description: The union of a set of positive reals (if a positive real) is its supremum (the least upper bound). 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	suplem2pr	|- ( A C_ P. -> ( ( y e. A -> -. U. A E. z e. A y

Proof

Step	Hyp	Ref	Expression
1		ltrelpr	|-
2	1	brel	|- ( y ( y e. P. /\ U. A e. P. ) )
3	2	simpld	|- ( y y e. P. )
4		ralnex	|- ( A. z e. A -. y -. E. z e. A y
5		ssel2	|- ( ( A C_ P. /\ z e. A ) -> z e. P. )
6		ltsopr	|-
7		sotric	|- ( ( ( y -. ( y = z \/ z
8	6 7	mpan	|- ( ( y e. P. /\ z e. P. ) -> ( y -. ( y = z \/ z
9	8	con2bid	|- ( ( y e. P. /\ z e. P. ) -> ( ( y = z \/ z -. y
10	9	ancoms	|- ( ( z e. P. /\ y e. P. ) -> ( ( y = z \/ z -. y
11		ltprord	|- ( ( z e. P. /\ y e. P. ) -> ( z z C. y ) )
12	11	orbi2d	|- ( ( z e. P. /\ y e. P. ) -> ( ( y = z \/ z ( y = z \/ z C. y ) ) )
13		sspss	|- ( z C_ y <-> ( z C. y \/ z = y ) )
14		equcom	|- ( z = y <-> y = z )
15	14	orbi2i	|- ( ( z C. y \/ z = y ) <-> ( z C. y \/ y = z ) )
16		orcom	|- ( ( z C. y \/ y = z ) <-> ( y = z \/ z C. y ) )
17	13 15 16	3bitri	|- ( z C_ y <-> ( y = z \/ z C. y ) )
18	12 17	bitr4di	|- ( ( z e. P. /\ y e. P. ) -> ( ( y = z \/ z z C_ y ) )
19	10 18	bitr3d	|- ( ( z e. P. /\ y e. P. ) -> ( -. y z C_ y ) )
20	5 19	sylan	|- ( ( ( A C_ P. /\ z e. A ) /\ y e. P. ) -> ( -. y z C_ y ) )
21	20	an32s	|- ( ( ( A C_ P. /\ y e. P. ) /\ z e. A ) -> ( -. y z C_ y ) )
22	21	ralbidva	|- ( ( A C_ P. /\ y e. P. ) -> ( A. z e. A -. y A. z e. A z C_ y ) )
23	4 22	bitr3id	|- ( ( A C_ P. /\ y e. P. ) -> ( -. E. z e. A y A. z e. A z C_ y ) )
24		unissb	|- ( U. A C_ y <-> A. z e. A z C_ y )
25	23 24	bitr4di	|- ( ( A C_ P. /\ y e. P. ) -> ( -. E. z e. A y U. A C_ y ) )
26		ssnpss	|- ( U. A C_ y -> -. y C. U. A )
27		ltprord	|- ( ( y e. P. /\ U. A e. P. ) -> ( y y C. U. A ) )
28	27	biimpd	|- ( ( y e. P. /\ U. A e. P. ) -> ( y y C. U. A ) )
29	2 28	mpcom	|- ( y y C. U. A )
30	26 29	nsyl	|- ( U. A C_ y -> -. y
31	25 30	syl6bi	|- ( ( A C_ P. /\ y e. P. ) -> ( -. E. z e. A y -. y
32	31	con4d	|- ( ( A C_ P. /\ y e. P. ) -> ( y E. z e. A y
33	32	ex	|- ( A C_ P. -> ( y e. P. -> ( y E. z e. A y
34	3 33	syl5	|- ( A C_ P. -> ( y ( y E. z e. A y
35	34	pm2.43d	|- ( A C_ P. -> ( y E. z e. A y
36		elssuni	|- ( y e. A -> y C_ U. A )
37		ssnpss	|- ( y C_ U. A -> -. U. A C. y )
38	36 37	syl	|- ( y e. A -> -. U. A C. y )
39	1	brel	|- ( U. A ( U. A e. P. /\ y e. P. ) )
40		ltprord	|- ( ( U. A e. P. /\ y e. P. ) -> ( U. A U. A C. y ) )
41	40	biimpd	|- ( ( U. A e. P. /\ y e. P. ) -> ( U. A U. A C. y ) )
42	39 41	mpcom	|- ( U. A U. A C. y )
43	38 42	nsyl	|- ( y e. A -> -. U. A
44	35 43	jctil	|- ( A C_ P. -> ( ( y e. A -> -. U. A E. z e. A y