Metamath Proof Explorer

Theorem suprleubrnmpt

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

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

Proof

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