Metamath Proof Explorer

Theorem infrpgernmpt

Description: The infimum of a nonempty, bounded below, indexed subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 infrpgernmpt.x 
 |-  F/ x ph
2 infrpgernmpt.a 
 |-  ( ph -> A =/= (/) )
3 infrpgernmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
4 infrpgernmpt.y 
 |-  ( ph -> E. y e. RR A. x e. A y <_ B )
5 infrpgernmpt.c 
 |-  ( ph -> C e. RR+ )
6 nfv 
 |-  F/ w ph
7 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
8 1 7 3 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR* )
9 1 3 7 2 rnmptn0 
 |-  ( ph -> ran ( x e. A |-> B ) =/= (/) )
10 breq1 
 |-  ( y = w -> ( y <_ B <-> w <_ B ) )
11 10 ralbidv 
 |-  ( y = w -> ( A. x e. A y <_ B <-> A. x e. A w <_ B ) )
12 11 cbvrexvw 
 |-  ( E. y e. RR A. x e. A y <_ B <-> E. w e. RR A. x e. A w <_ B )
13 4 12 sylib 
 |-  ( ph -> E. w e. RR A. x e. A w <_ B )
14 13 rnmptlb 
 |-  ( ph -> E. w e. RR A. z e. ran ( x e. A |-> B ) w <_ z )
15 6 8 9 14 5 infrpge 
 |-  ( ph -> E. w e. ran ( x e. A |-> B ) w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) )
16 simpll 
 |-  ( ( ( ph /\ w e. ran ( x e. A |-> B ) ) /\ w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) -> ph )
17 simpr 
 |-  ( ( ( ph /\ w e. ran ( x e. A |-> B ) ) /\ w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) -> w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) )
18 vex 
 |-  w e. _V
19 7 elrnmpt 
 |-  ( w e. _V -> ( w e. ran ( x e. A |-> B ) <-> E. x e. A w = B ) )
20 18 19 ax-mp 
 |-  ( w e. ran ( x e. A |-> B ) <-> E. x e. A w = B )
21 20 biimpi 
 |-  ( w e. ran ( x e. A |-> B ) -> E. x e. A w = B )
22 21 ad2antlr 
 |-  ( ( ( ph /\ w e. ran ( x e. A |-> B ) ) /\ w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) -> E. x e. A w = B )
23 nfcv 
 |-  F/_ x w
24 nfcv 
 |-  F/_ x <_
25 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
26 25 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
27 nfcv 
 |-  F/_ x RR*
28 nfcv 
 |-  F/_ x <
29 26 27 28 nfinf 
 |-  F/_ x inf ( ran ( x e. A |-> B ) , RR* , < )
30 nfcv 
 |-  F/_ x +e
31 nfcv 
 |-  F/_ x C
32 29 30 31 nfov 
 |-  F/_ x ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C )
33 23 24 32 nfbr 
 |-  F/ x w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C )
34 1 33 nfan 
 |-  F/ x ( ph /\ w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) )
35 id 
 |-  ( w = B -> w = B )
36 35 eqcomd 
 |-  ( w = B -> B = w )
37 36 adantl 
 |-  ( ( w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) /\ w = B ) -> B = w )
38 simpl 
 |-  ( ( w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) /\ w = B ) -> w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) )
39 37 38 eqbrtrd 
 |-  ( ( w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) /\ w = B ) -> B <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) )
40 39 ex 
 |-  ( w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) -> ( w = B -> B <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) )
41 40 a1d 
 |-  ( w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) -> ( x e. A -> ( w = B -> B <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) ) )
42 41 adantl 
 |-  ( ( ph /\ w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) -> ( x e. A -> ( w = B -> B <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) ) )
43 34 42 reximdai 
 |-  ( ( ph /\ w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) -> ( E. x e. A w = B -> E. x e. A B <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) )
44 43 imp 
 |-  ( ( ( ph /\ w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) /\ E. x e. A w = B ) -> E. x e. A B <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) )
45 16 17 22 44 syl21anc 
 |-  ( ( ( ph /\ w e. ran ( x e. A |-> B ) ) /\ w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) -> E. x e. A B <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) )
46 45 rexlimdva2 
 |-  ( ph -> ( E. w e. ran ( x e. A |-> B ) w <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) -> E. x e. A B <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) ) )
47 15 46 mpd 
 |-  ( ph -> E. x e. A B <_ ( inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) )