Metamath Proof Explorer

Theorem upbdrech

Description: Choice of an upper bound for a nonempty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses upbdrech.a 
|- ( ph -> A =/= (/) )
upbdrech.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
upbdrech.bd 
|- ( ph -> E. y e. RR A. x e. A B <_ y )
upbdrech.c 
|- C = sup ( { z | E. x e. A z = B } , RR , < )
Assertion upbdrech 
|- ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )

Proof

Step Hyp Ref Expression
1 upbdrech.a 
 |-  ( ph -> A =/= (/) )
2 upbdrech.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
3 upbdrech.bd 
 |-  ( ph -> E. y e. RR A. x e. A B <_ y )
4 upbdrech.c 
 |-  C = sup ( { z | E. x e. A z = B } , RR , < )
5 2 ralrimiva 
 |-  ( ph -> A. x e. A B e. RR )
6 nfra1 
 |-  F/ x A. x e. A B e. RR
7 nfv 
 |-  F/ x z e. RR
8 simp3 
 |-  ( ( A. x e. A B e. RR /\ x e. A /\ z = B ) -> z = B )
9 rspa 
 |-  ( ( A. x e. A B e. RR /\ x e. A ) -> B e. RR )
10 9 3adant3 
 |-  ( ( A. x e. A B e. RR /\ x e. A /\ z = B ) -> B e. RR )
11 8 10 eqeltrd 
 |-  ( ( A. x e. A B e. RR /\ x e. A /\ z = B ) -> z e. RR )
12 11 3exp 
 |-  ( A. x e. A B e. RR -> ( x e. A -> ( z = B -> z e. RR ) ) )
13 6 7 12 rexlimd 
 |-  ( A. x e. A B e. RR -> ( E. x e. A z = B -> z e. RR ) )
14 13 abssdv 
 |-  ( A. x e. A B e. RR -> { z | E. x e. A z = B } C_ RR )
15 5 14 syl 
 |-  ( ph -> { z | E. x e. A z = B } C_ RR )
16 eqidd 
 |-  ( x e. A -> B = B )
17 16 rgen 
 |-  A. x e. A B = B
18 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A B = B ) -> E. x e. A B = B )
19 1 17 18 sylancl 
 |-  ( ph -> E. x e. A B = B )
20 nfv 
 |-  F/ x ph
21 nfre1 
 |-  F/ x E. x e. A z = B
22 21 nfex 
 |-  F/ x E. z E. x e. A z = B
23 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
24 elex 
 |-  ( B e. RR -> B e. _V )
25 2 24 syl 
 |-  ( ( ph /\ x e. A ) -> B e. _V )
26 isset 
 |-  ( B e. _V <-> E. z z = B )
27 25 26 sylib 
 |-  ( ( ph /\ x e. A ) -> E. z z = B )
28 rspe 
 |-  ( ( x e. A /\ E. z z = B ) -> E. x e. A E. z z = B )
29 23 27 28 syl2anc 
 |-  ( ( ph /\ x e. A ) -> E. x e. A E. z z = B )
30 rexcom4 
 |-  ( E. x e. A E. z z = B <-> E. z E. x e. A z = B )
31 29 30 sylib 
 |-  ( ( ph /\ x e. A ) -> E. z E. x e. A z = B )
32 31 3adant3 
 |-  ( ( ph /\ x e. A /\ B = B ) -> E. z E. x e. A z = B )
33 32 3exp 
 |-  ( ph -> ( x e. A -> ( B = B -> E. z E. x e. A z = B ) ) )
34 20 22 33 rexlimd 
 |-  ( ph -> ( E. x e. A B = B -> E. z E. x e. A z = B ) )
35 19 34 mpd 
 |-  ( ph -> E. z E. x e. A z = B )
36 abn0 
 |-  ( { z | E. x e. A z = B } =/= (/) <-> E. z E. x e. A z = B )
37 35 36 sylibr 
 |-  ( ph -> { z | E. x e. A z = B } =/= (/) )
38 vex 
 |-  w e. _V
39 eqeq1 
 |-  ( z = w -> ( z = B <-> w = B ) )
40 39 rexbidv 
 |-  ( z = w -> ( E. x e. A z = B <-> E. x e. A w = B ) )
41 38 40 elab 
 |-  ( w e. { z | E. x e. A z = B } <-> E. x e. A w = B )
42 41 biimpi 
 |-  ( w e. { z | E. x e. A z = B } -> E. x e. A w = B )
43 42 adantl 
 |-  ( ( ( ph /\ A. x e. A B <_ y ) /\ w e. { z | E. x e. A z = B } ) -> E. x e. A w = B )
44 nfra1 
 |-  F/ x A. x e. A B <_ y
45 20 44 nfan 
 |-  F/ x ( ph /\ A. x e. A B <_ y )
46 21 nfsab 
 |-  F/ x w e. { z | E. x e. A z = B }
47 45 46 nfan 
 |-  F/ x ( ( ph /\ A. x e. A B <_ y ) /\ w e. { z | E. x e. A z = B } )
48 nfv 
 |-  F/ x w <_ y
49 simp3 
 |-  ( ( ( ph /\ A. x e. A B <_ y ) /\ x e. A /\ w = B ) -> w = B )
50 simp1r 
 |-  ( ( ( ph /\ A. x e. A B <_ y ) /\ x e. A /\ w = B ) -> A. x e. A B <_ y )
51 simp2 
 |-  ( ( ( ph /\ A. x e. A B <_ y ) /\ x e. A /\ w = B ) -> x e. A )
52 rspa 
 |-  ( ( A. x e. A B <_ y /\ x e. A ) -> B <_ y )
53 50 51 52 syl2anc 
 |-  ( ( ( ph /\ A. x e. A B <_ y ) /\ x e. A /\ w = B ) -> B <_ y )
54 49 53 eqbrtrd 
 |-  ( ( ( ph /\ A. x e. A B <_ y ) /\ x e. A /\ w = B ) -> w <_ y )
55 54 3exp 
 |-  ( ( ph /\ A. x e. A B <_ y ) -> ( x e. A -> ( w = B -> w <_ y ) ) )
56 55 adantr 
 |-  ( ( ( ph /\ A. x e. A B <_ y ) /\ w e. { z | E. x e. A z = B } ) -> ( x e. A -> ( w = B -> w <_ y ) ) )
57 47 48 56 rexlimd 
 |-  ( ( ( ph /\ A. x e. A B <_ y ) /\ w e. { z | E. x e. A z = B } ) -> ( E. x e. A w = B -> w <_ y ) )
58 43 57 mpd 
 |-  ( ( ( ph /\ A. x e. A B <_ y ) /\ w e. { z | E. x e. A z = B } ) -> w <_ y )
59 58 ralrimiva 
 |-  ( ( ph /\ A. x e. A B <_ y ) -> A. w e. { z | E. x e. A z = B } w <_ y )
60 59 3adant2 
 |-  ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) -> A. w e. { z | E. x e. A z = B } w <_ y )
61 60 3exp 
 |-  ( ph -> ( y e. RR -> ( A. x e. A B <_ y -> A. w e. { z | E. x e. A z = B } w <_ y ) ) )
62 61 reximdvai 
 |-  ( ph -> ( E. y e. RR A. x e. A B <_ y -> E. y e. RR A. w e. { z | E. x e. A z = B } w <_ y ) )
63 3 62 mpd 
 |-  ( ph -> E. y e. RR A. w e. { z | E. x e. A z = B } w <_ y )
64 suprcl 
 |-  ( ( { z | E. x e. A z = B } C_ RR /\ { z | E. x e. A z = B } =/= (/) /\ E. y e. RR A. w e. { z | E. x e. A z = B } w <_ y ) -> sup ( { z | E. x e. A z = B } , RR , < ) e. RR )
65 15 37 63 64 syl3anc 
 |-  ( ph -> sup ( { z | E. x e. A z = B } , RR , < ) e. RR )
66 4 65 eqeltrid 
 |-  ( ph -> C e. RR )
67 15 adantr 
 |-  ( ( ph /\ x e. A ) -> { z | E. x e. A z = B } C_ RR )
68 31 36 sylibr 
 |-  ( ( ph /\ x e. A ) -> { z | E. x e. A z = B } =/= (/) )
69 63 adantr 
 |-  ( ( ph /\ x e. A ) -> E. y e. RR A. w e. { z | E. x e. A z = B } w <_ y )
70 elabrexg 
 |-  ( ( x e. A /\ B e. RR ) -> B e. { z | E. x e. A z = B } )
71 23 2 70 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. { z | E. x e. A z = B } )
72 suprub 
 |-  ( ( ( { z | E. x e. A z = B } C_ RR /\ { z | E. x e. A z = B } =/= (/) /\ E. y e. RR A. w e. { z | E. x e. A z = B } w <_ y ) /\ B e. { z | E. x e. A z = B } ) -> B <_ sup ( { z | E. x e. A z = B } , RR , < ) )
73 67 68 69 71 72 syl31anc 
 |-  ( ( ph /\ x e. A ) -> B <_ sup ( { z | E. x e. A z = B } , RR , < ) )
74 73 4 breqtrrdi 
 |-  ( ( ph /\ x e. A ) -> B <_ C )
75 74 ralrimiva 
 |-  ( ph -> A. x e. A B <_ C )
76 66 75 jca 
 |-  ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )