Metamath Proof Explorer

Theorem supxrleubrnmpt

Description: The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses supxrleubrnmpt.x 
|- F/ x ph
supxrleubrnmpt.b 
|- ( ( ph /\ x e. A ) -> B e. RR* )
supxrleubrnmpt.c 
|- ( ph -> C e. RR* )
Assertion supxrleubrnmpt 
|- ( ph -> ( sup ( ran ( x e. A |-> B ) , RR* , < ) <_ C <-> A. x e. A B <_ C ) )

Proof

Step Hyp Ref Expression
1 supxrleubrnmpt.x 
 |-  F/ x ph
2 supxrleubrnmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
3 supxrleubrnmpt.c 
 |-  ( ph -> C e. RR* )
4 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
5 1 4 2 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR* )
6 supxrleub 
 |-  ( ( ran ( x e. A |-> B ) C_ RR* /\ C e. RR* ) -> ( sup ( ran ( x e. A |-> B ) , RR* , < ) <_ C <-> A. z e. ran ( x e. A |-> B ) z <_ C ) )
7 5 3 6 syl2anc 
 |-  ( ph -> ( sup ( ran ( x e. A |-> B ) , RR* , < ) <_ C <-> A. z e. ran ( x e. A |-> B ) z <_ C ) )
8 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
9 8 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
10 nfv 
 |-  F/ x z <_ C
11 9 10 nfralw 
 |-  F/ x A. z e. ran ( x e. A |-> B ) z <_ C
12 1 11 nfan 
 |-  F/ x ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ C )
13 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
14 4 elrnmpt1 
 |-  ( ( x e. A /\ B e. RR* ) -> B e. ran ( x e. A |-> B ) )
15 13 2 14 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
16 15 adantlr 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ C ) /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
17 simplr 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ C ) /\ x e. A ) -> A. z e. ran ( x e. A |-> B ) z <_ C )
18 breq1 
 |-  ( z = B -> ( z <_ C <-> B <_ C ) )
19 18 rspcva 
 |-  ( ( B e. ran ( x e. A |-> B ) /\ A. z e. ran ( x e. A |-> B ) z <_ C ) -> B <_ C )
20 16 17 19 syl2anc 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ C ) /\ x e. A ) -> B <_ C )
21 20 ex 
 |-  ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ C ) -> ( x e. A -> B <_ C ) )
22 12 21 ralrimi 
 |-  ( ( ph /\ A. z e. ran ( x e. A |-> B ) z <_ C ) -> A. x e. A B <_ C )
23 22 ex 
 |-  ( ph -> ( A. z e. ran ( x e. A |-> B ) z <_ C -> A. x e. A B <_ C ) )
24 vex 
 |-  z e. _V
25 4 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B ) )
26 24 25 ax-mp 
 |-  ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B )
27 26 biimpi 
 |-  ( z e. ran ( x e. A |-> B ) -> E. x e. A z = B )
28 27 adantl 
 |-  ( ( A. x e. A B <_ C /\ z e. ran ( x e. A |-> B ) ) -> E. x e. A z = B )
29 nfra1 
 |-  F/ x A. x e. A B <_ C
30 rspa 
 |-  ( ( A. x e. A B <_ C /\ x e. A ) -> B <_ C )
31 18 biimprcd 
 |-  ( B <_ C -> ( z = B -> z <_ C ) )
32 30 31 syl 
 |-  ( ( A. x e. A B <_ C /\ x e. A ) -> ( z = B -> z <_ C ) )
33 32 ex 
 |-  ( A. x e. A B <_ C -> ( x e. A -> ( z = B -> z <_ C ) ) )
34 29 10 33 rexlimd 
 |-  ( A. x e. A B <_ C -> ( E. x e. A z = B -> z <_ C ) )
35 34 adantr 
 |-  ( ( A. x e. A B <_ C /\ z e. ran ( x e. A |-> B ) ) -> ( E. x e. A z = B -> z <_ C ) )
36 28 35 mpd 
 |-  ( ( A. x e. A B <_ C /\ z e. ran ( x e. A |-> B ) ) -> z <_ C )
37 36 ralrimiva 
 |-  ( A. x e. A B <_ C -> A. z e. ran ( x e. A |-> B ) z <_ C )
38 37 a1i 
 |-  ( ph -> ( A. x e. A B <_ C -> A. z e. ran ( x e. A |-> B ) z <_ C ) )
39 23 38 impbid 
 |-  ( ph -> ( A. z e. ran ( x e. A |-> B ) z <_ C <-> A. x e. A B <_ C ) )
40 7 39 bitrd 
 |-  ( ph -> ( sup ( ran ( x e. A |-> B ) , RR* , < ) <_ C <-> A. x e. A B <_ C ) )