Metamath Proof Explorer

Theorem supxrleubrnmptf

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, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 supxrleubrnmptf.x 
 |-  F/ x ph
2 supxrleubrnmptf.a 
 |-  F/_ x A
3 supxrleubrnmptf.n 
 |-  F/_ x C
4 supxrleubrnmptf.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
5 supxrleubrnmptf.c 
 |-  ( ph -> C e. RR* )
6 nfcv 
 |-  F/_ y A
7 nfcv 
 |-  F/_ y B
8 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
9 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
10 2 6 7 8 9 cbvmptf 
 |-  ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
11 10 rneqi 
 |-  ran ( x e. A |-> B ) = ran ( y e. A |-> [_ y / x ]_ B )
12 11 supeq1i 
 |-  sup ( ran ( x e. A |-> B ) , RR* , < ) = sup ( ran ( y e. A |-> [_ y / x ]_ B ) , RR* , < )
13 12 breq1i 
 |-  ( sup ( ran ( x e. A |-> B ) , RR* , < ) <_ C <-> sup ( ran ( y e. A |-> [_ y / x ]_ B ) , RR* , < ) <_ C )
14 13 a1i 
 |-  ( ph -> ( sup ( ran ( x e. A |-> B ) , RR* , < ) <_ C <-> sup ( ran ( y e. A |-> [_ y / x ]_ B ) , RR* , < ) <_ C ) )
15 nfv 
 |-  F/ y ph
16 2 nfcri 
 |-  F/ x y e. A
17 1 16 nfan 
 |-  F/ x ( ph /\ y e. A )
18 8 nfel1 
 |-  F/ x [_ y / x ]_ B e. RR*
19 17 18 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. RR* )
20 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
21 20 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. A ) <-> ( ph /\ y e. A ) ) )
22 9 eleq1d 
 |-  ( x = y -> ( B e. RR* <-> [_ y / x ]_ B e. RR* ) )
23 21 22 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> B e. RR* ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. RR* ) ) )
24 19 23 4 chvarfv 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. RR* )
25 15 24 5 supxrleubrnmpt 
 |-  ( ph -> ( sup ( ran ( y e. A |-> [_ y / x ]_ B ) , RR* , < ) <_ C <-> A. y e. A [_ y / x ]_ B <_ C ) )
26 nfcv 
 |-  F/_ x <_
27 8 26 3 nfbr 
 |-  F/ x [_ y / x ]_ B <_ C
28 nfv 
 |-  F/ y B <_ C
29 eqcom 
 |-  ( x = y <-> y = x )
30 29 imbi1i 
 |-  ( ( x = y -> B = [_ y / x ]_ B ) <-> ( y = x -> B = [_ y / x ]_ B ) )
31 eqcom 
 |-  ( B = [_ y / x ]_ B <-> [_ y / x ]_ B = B )
32 31 imbi2i 
 |-  ( ( y = x -> B = [_ y / x ]_ B ) <-> ( y = x -> [_ y / x ]_ B = B ) )
33 30 32 bitri 
 |-  ( ( x = y -> B = [_ y / x ]_ B ) <-> ( y = x -> [_ y / x ]_ B = B ) )
34 9 33 mpbi 
 |-  ( y = x -> [_ y / x ]_ B = B )
35 34 breq1d 
 |-  ( y = x -> ( [_ y / x ]_ B <_ C <-> B <_ C ) )
36 6 2 27 28 35 cbvralfw 
 |-  ( A. y e. A [_ y / x ]_ B <_ C <-> A. x e. A B <_ C )
37 36 a1i 
 |-  ( ph -> ( A. y e. A [_ y / x ]_ B <_ C <-> A. x e. A B <_ C ) )
38 14 25 37 3bitrd 
 |-  ( ph -> ( sup ( ran ( x e. A |-> B ) , RR* , < ) <_ C <-> A. x e. A B <_ C ) )