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 biimpi 
 |-  ( z e. ran F -> E. x e. A z = B )
20 19 adantl 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) /\ z e. ran F ) -> E. x e. A z = B )
21 simp3 
 |-  ( ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B ) -> E. x e. A z = B )
22 nfra1 
 |-  F/ x A. x e. A B <_ y
23 nfre1 
 |-  F/ x E. x e. A z = B
24 9 22 23 nf3an 
 |-  F/ x ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B )
25 nfv 
 |-  F/ x z <_ y
26 simp3 
 |-  ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> z = B )
27 rspa 
 |-  ( ( A. x e. A B <_ y /\ x e. A ) -> B <_ y )
28 27 3adant3 
 |-  ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> B <_ y )
29 26 28 eqbrtrd 
 |-  ( ( A. x e. A B <_ y /\ x e. A /\ z = B ) -> z <_ y )
30 29 3exp 
 |-  ( A. x e. A B <_ y -> ( x e. A -> ( z = B -> z <_ y ) ) )
31 30 3ad2ant2 
 |-  ( ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B ) -> ( x e. A -> ( z = B -> z <_ y ) ) )
32 24 25 31 rexlimd 
 |-  ( ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B ) -> ( E. x e. A z = B -> z <_ y ) )
33 21 32 mpd 
 |-  ( ( ph /\ A. x e. A B <_ y /\ E. x e. A z = B ) -> z <_ y )
34 14 15 20 33 syl3anc 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) /\ z e. ran F ) -> z <_ y )
35 34 ralrimiva 
 |-  ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) -> A. z e. ran F z <_ y )
36 19.8a 
 |-  ( ( y e. RR /\ A. z e. ran F z <_ y ) -> E. y ( y e. RR /\ A. z e. ran F z <_ y ) )
37 13 35 36 syl2anc 
 |-  ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) -> E. y ( y e. RR /\ A. z e. ran F z <_ y ) )
38 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 ) )
39 37 38 sylibr 
 |-  ( ( ph /\ y e. RR /\ A. x e. A B <_ y ) -> E. y e. RR A. z e. ran F z <_ y )
40 39 3exp 
 |-  ( ph -> ( y e. RR -> ( A. x e. A B <_ y -> E. y e. RR A. z e. ran F z <_ y ) ) )
41 11 12 40 rexlimd 
 |-  ( ph -> ( E. y e. RR A. x e. A B <_ y -> E. y e. RR A. z e. ran F z <_ y ) )
42 3 41 mpd 
 |-  ( ph -> E. y e. RR A. z e. ran F z <_ y )
43 suprcl 
 |-  ( ( ran F C_ RR /\ ran F =/= (/) /\ E. y e. RR A. z e. ran F z <_ y ) -> sup ( ran F , RR , < ) e. RR )
44 8 10 42 43 syl3anc 
 |-  ( ph -> sup ( ran F , RR , < ) e. RR )
45 5 44 eqeltrid 
 |-  ( ph -> C e. RR )
46 8 adantr 
 |-  ( ( ph /\ x e. A ) -> ran F C_ RR )
47 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
48 4 elrnmpt1 
 |-  ( ( x e. A /\ B e. RR ) -> B e. ran F )
49 47 2 48 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. ran F )
50 49 ne0d 
 |-  ( ( ph /\ x e. A ) -> ran F =/= (/) )
51 42 adantr 
 |-  ( ( ph /\ x e. A ) -> E. y e. RR A. z e. ran F z <_ y )
52 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 , < ) )
53 46 50 51 49 52 syl31anc 
 |-  ( ( ph /\ x e. A ) -> B <_ sup ( ran F , RR , < ) )
54 53 5 breqtrrdi 
 |-  ( ( ph /\ x e. A ) -> B <_ C )
55 54 ralrimiva 
 |-  ( ph -> A. x e. A B <_ C )
56 45 55 jca 
 |-  ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )