Metamath Proof Explorer

Theorem infxrgelbrnmpt

Description: The infimum of an indexed set of extended reals is greater than or equal to a lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 infxrgelbrnmpt.x 
 |-  F/ x ph
2 infxrgelbrnmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
3 infxrgelbrnmpt.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 infxrgelb 
 |-  ( ( ran ( x e. A |-> B ) C_ RR* /\ C e. RR* ) -> ( C <_ inf ( ran ( x e. A |-> B ) , RR* , < ) <-> A. z e. ran ( x e. A |-> B ) C <_ z ) )
7 5 3 6 syl2anc 
 |-  ( ph -> ( C <_ inf ( ran ( x e. A |-> B ) , RR* , < ) <-> A. z e. ran ( x e. A |-> B ) C <_ z ) )
8 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
9 8 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
10 nfv 
 |-  F/ x C <_ z
11 9 10 nfralw 
 |-  F/ x A. z e. ran ( x e. A |-> B ) C <_ z
12 1 11 nfan 
 |-  F/ x ( ph /\ A. z e. ran ( x e. A |-> B ) C <_ z )
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 ) C <_ z ) /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
17 simplr 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) C <_ z ) /\ x e. A ) -> A. z e. ran ( x e. A |-> B ) C <_ z )
18 breq2 
 |-  ( z = B -> ( C <_ z <-> C <_ B ) )
19 18 rspcva 
 |-  ( ( B e. ran ( x e. A |-> B ) /\ A. z e. ran ( x e. A |-> B ) C <_ z ) -> C <_ B )
20 16 17 19 syl2anc 
 |-  ( ( ( ph /\ A. z e. ran ( x e. A |-> B ) C <_ z ) /\ x e. A ) -> C <_ B )
21 20 ex 
 |-  ( ( ph /\ A. z e. ran ( x e. A |-> B ) C <_ z ) -> ( x e. A -> C <_ B ) )
22 12 21 ralrimi 
 |-  ( ( ph /\ A. z e. ran ( x e. A |-> B ) C <_ z ) -> A. x e. A C <_ B )
23 vex 
 |-  z e. _V
24 4 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B ) )
25 23 24 ax-mp 
 |-  ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B )
26 25 biimpi 
 |-  ( z e. ran ( x e. A |-> B ) -> E. x e. A z = B )
27 26 adantl 
 |-  ( ( A. x e. A C <_ B /\ z e. ran ( x e. A |-> B ) ) -> E. x e. A z = B )
28 nfra1 
 |-  F/ x A. x e. A C <_ B
29 rspa 
 |-  ( ( A. x e. A C <_ B /\ x e. A ) -> C <_ B )
30 18 biimprcd 
 |-  ( C <_ B -> ( z = B -> C <_ z ) )
31 29 30 syl 
 |-  ( ( A. x e. A C <_ B /\ x e. A ) -> ( z = B -> C <_ z ) )
32 31 ex 
 |-  ( A. x e. A C <_ B -> ( x e. A -> ( z = B -> C <_ z ) ) )
33 28 10 32 rexlimd 
 |-  ( A. x e. A C <_ B -> ( E. x e. A z = B -> C <_ z ) )
34 33 adantr 
 |-  ( ( A. x e. A C <_ B /\ z e. ran ( x e. A |-> B ) ) -> ( E. x e. A z = B -> C <_ z ) )
35 27 34 mpd 
 |-  ( ( A. x e. A C <_ B /\ z e. ran ( x e. A |-> B ) ) -> C <_ z )
36 35 ralrimiva 
 |-  ( A. x e. A C <_ B -> A. z e. ran ( x e. A |-> B ) C <_ z )
37 36 adantl 
 |-  ( ( ph /\ A. x e. A C <_ B ) -> A. z e. ran ( x e. A |-> B ) C <_ z )
38 22 37 impbida 
 |-  ( ph -> ( A. z e. ran ( x e. A |-> B ) C <_ z <-> A. x e. A C <_ B ) )
39 7 38 bitrd 
 |-  ( ph -> ( C <_ inf ( ran ( x e. A |-> B ) , RR* , < ) <-> A. x e. A C <_ B ) )