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