This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi 
 |-  ( ( 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