Metamath Proof Explorer

Theorem suprnmpt

Description: An explicit bound for the range of a bounded function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses suprnmpt.a 
|- ( ph -> A =/= (/) )
suprnmpt.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
suprnmpt.bnd 
|- ( ph -> E. y e. RR A. x e. A B <_ y )
suprnmpt.f 
|- F = ( x e. A |-> B )
suprnmpt.c 
|- C = sup ( ran F , RR , < )
Assertion suprnmpt 
|- ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )

Proof

Step Hyp Ref Expression
1 suprnmpt.a 
 |-  ( ph -> A =/= (/) )
2 suprnmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
3 suprnmpt.bnd 
 |-  ( ph -> E. y e. RR A. x e. A B <_ y )
4 suprnmpt.f 
 |-  F = ( x e. A |-> B )
5 suprnmpt.c 
 |-  C = sup ( ran F , RR , < )
6 2 ralrimiva 
 |-  ( ph -> A. x e. A B e. RR )
7 4 rnmptss 
 |-  ( A. x e. A B e. RR -> ran F C_ RR )
8 6 7 syl 
 |-  ( ph -> ran F C_ RR )
9 nfv 
 |-  F/ x ph
10 9 2 4 1 rnmptn0 
 |-  ( ph -> ran F =/= (/) )
11 nfv 
 |-  F/ y ph
12 nfre1 
 |-  F/ y E. y e. RR A. z e. ran F z <_ y
13 simp2 
 |-  ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) -> y e. RR )
14 simpl1 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) /\ z e. ran F ) -> ph )
15 simpl3 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) /\ z e. ran F ) -> A. x e. A B <_ y )
16 vex 
 |-  z e. _V
17 4 elrnmpt 
 |-  ( z e. _V -> ( z e. ran F <-> E. x e. A z = B ) )
18 16 17 ax-mp 
 |-  ( z e. ran F <-> E. x e. A z = B )
19 18 bilani 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) /\ z e. ran F ) -> E. x e. A z = B )
20 simp3 
 |-  ( ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B ) -> E. x e. A z = B )
21 nfra1 
 |-  F/ x A. x e. A B <_ y
22 nfre1 
 |-  F/ x E. x e. A z = B
23 9 21 22 nf3an 
 |-  F/ x ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B )
24 nfv 
 |-  F/ x z <_ y
25 simp3 
 |-  ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> z = B )
26 rspa 
 |-  ( ( A. x e. A B <_ y /\ x e. A ) -> B <_ y )
27 26 3adant3 
 |-  ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> B <_ y )
28 25 27 eqbrtrd 
 |-  ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> z <_ y )
29 28 3exp 
 |-  ( A. x e. A B <_ y -> ( x e. A -> ( z = B -> z <_ y ) ) )
30 29 3ad2ant2 
 |-  ( ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B ) -> ( x e. A -> ( z = B -> z <_ y ) ) )
31 23 24 30 rexlimd 
 |-  ( ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B ) -> ( E. x e. A z = B -> z <_ y ) )
32 20 31 mpd 
 |-  ( ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B ) -> z <_ y )
33 14 15 19 32 syl3anc 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) /\ z e. ran F ) -> z <_ y )
34 33 ralrimiva 
 |-  ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) -> A. z e. ran F z <_ y )
35 19.8a 
 |-  ( ( y e. RR /\ A. z e. ran F z <_ y ) -> E. y ( y e. RR /\ A. z e. ran F z <_ y ) )
36 13 34 35 syl2anc 
 |-  ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) -> E. y ( y e. RR /\ A. z e. ran F z <_ y ) )
37 df-rex 
 |-  ( E. y e. RR A. z e. ran F z <_ y <-> E. y ( y e. RR /\ A. z e. ran F z <_ y ) )
38 36 37 sylibr 
 |-  ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) -> E. y e. RR A. z e. ran F z <_ y )
39 38 3exp 
 |-  ( ph -> ( y e. RR -> ( A. x e. A B <_ y -> E. y e. RR A. z e. ran F z <_ y ) ) )
40 11 12 39 rexlimd 
 |-  ( ph -> ( E. y e. RR A. x e. A B <_ y -> E. y e. RR A. z e. ran F z <_ y ) )
41 3 40 mpd 
 |-  ( ph -> E. y e. RR A. z e. ran F z <_ y )
42 suprcl 
 |-  ( ( ran F C_ RR /\ ran F =/= (/) /\ E. y e. RR A. z e. ran F z <_ y ) -> sup ( ran F , RR , < ) e. RR )
43 8 10 41 42 syl3anc 
 |-  ( ph -> sup ( ran F , RR , < ) e. RR )
44 5 43 eqeltrid 
 |-  ( ph -> C e. RR )
45 8 adantr 
 |-  ( ( ph /\ x e. A ) -> ran F C_ RR )
46 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
47 4 elrnmpt1 
 |-  ( ( x e. A /\ B e. RR ) -> B e. ran F )
48 46 2 47 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. ran F )
49 48 ne0d 
 |-  ( ( ph /\ x e. A ) -> ran F =/= (/) )
50 41 adantr 
 |-  ( ( ph /\ x e. A ) -> E. y e. RR A. z e. ran F z <_ y )
51 suprub 
 |-  ( ( ( ran F C_ RR /\ ran F =/= (/) /\ E. y e. RR A. z e. ran F z <_ y ) /\ B e. ran F ) -> B <_ sup ( ran F , RR , < ) )
52 45 49 50 48 51 syl31anc 
 |-  ( ( ph /\ x e. A ) -> B <_ sup ( ran F , RR , < ) )
53 52 5 breqtrrdi 
 |-  ( ( ph /\ x e. A ) -> B <_ C )
54 53 ralrimiva 
 |-  ( ph -> A. x e. A B <_ C )
55 44 54 jca 
 |-  ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )