Metamath Proof Explorer

Theorem supexpr

Description: The union of a nonempty, bounded set of positive reals has a supremum. Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 19-May-1996) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 suplem1pr 
 |-  ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 U. A e. P. )
2 ltrelpr 
 |-
3 2 brel 
 |-  ( y 
 ( y e. P. /\ x e. P. ) )
4 3 simpld 
 |-  ( y 
 y e. P. )
5 4 ralimi 
 |-  ( A. y e. A y 
 A. y e. A y e. P. )
6 dfss3 
 |-  ( A C_ P. <-> A. y e. A y e. P. )
7 5 6 sylibr 
 |-  ( A. y e. A y 
 A C_ P. )
8 7 rexlimivw 
 |-  ( E. x e. P. A. y e. A y 
 A C_ P. )
9 8 adantl 
 |-  ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 A C_ P. )
10 suplem2pr 
 |-  ( A C_ P. -> ( ( y e. A -> -. U. A 
 E. z e. A y
11 10 simpld 
 |-  ( A C_ P. -> ( y e. A -> -. U. A
12 11 ralrimiv 
 |-  ( A C_ P. -> A. y e. A -. U. A
13 10 simprd 
 |-  ( A C_ P. -> ( y 
 E. z e. A y
14 13 ralrimivw 
 |-  ( A C_ P. -> A. y e. P. ( y 
 E. z e. A y
15 12 14 jca 
 |-  ( A C_ P. -> ( A. y e. A -. U. A 
 E. z e. A y
16 9 15 syl 
 |-  ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 ( A. y e. A -. U. A 
 E. z e. A y
17 breq1 
 |-  ( x = U. A -> ( x 
 U. A
18 17 notbid 
 |-  ( x = U. A -> ( -. x 
 -. U. A
19 18 ralbidv 
 |-  ( x = U. A -> ( A. y e. A -. x 
 A. y e. A -. U. A
20 breq2 
 |-  ( x = U. A -> ( y 
 y
21 20 imbi1d 
 |-  ( x = U. A -> ( ( y 
 E. z e. A y 
 ( y 
 E. z e. A y
22 21 ralbidv 
 |-  ( x = U. A -> ( A. y e. P. ( y 
 E. z e. A y 
 A. y e. P. ( y 
 E. z e. A y
23 19 22 anbi12d 
 |-  ( x = U. A -> ( ( A. y e. A -. x 
 E. z e. A y 
 ( A. y e. A -. U. A 
 E. z e. A y
24 23 rspcev 
 |-  ( ( U. A e. P. /\ ( A. y e. A -. U. A 
 E. z e. A y 
 E. x e. P. ( A. y e. A -. x 
 E. z e. A y
25 1 16 24 syl2anc 
 |-  ( ( A =/= (/) /\ E. x e. P. A. y e. A y 
 E. x e. P. ( A. y e. A -. x 
 E. z e. A y