Metamath Proof Explorer

Theorem infxrunb3rnmpt

Description: The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses infxrunb3rnmpt.1 
|- F/ x ph
infxrunb3rnmpt.2 
|- F/ y ph
infxrunb3rnmpt.3 
|- ( ( ph /\ x e. A ) -> B e. RR* )
Assertion infxrunb3rnmpt 
|- ( ph -> ( A. y e. RR E. x e. A B <_ y <-> inf ( ran ( x e. A |-> B ) , RR* , < ) = -oo ) )

Proof

Step Hyp Ref Expression
1 infxrunb3rnmpt.1 
 |-  F/ x ph
2 infxrunb3rnmpt.2 
 |-  F/ y ph
3 infxrunb3rnmpt.3 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
4 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
5 4 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
6 nfv 
 |-  F/ x z <_ y
7 5 6 nfrexw 
 |-  F/ x E. z e. ran ( x e. A |-> B ) z <_ y
8 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
9 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
10 9 elrnmpt1 
 |-  ( ( x e. A /\ B e. RR* ) -> B e. ran ( x e. A |-> B ) )
11 8 3 10 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
12 11 3adant3 
 |-  ( ( ph /\ x e. A /\ B <_ y ) -> B e. ran ( x e. A |-> B ) )
13 simp3 
 |-  ( ( ph /\ x e. A /\ B <_ y ) -> B <_ y )
14 breq1 
 |-  ( z = B -> ( z <_ y <-> B <_ y ) )
15 14 rspcev 
 |-  ( ( B e. ran ( x e. A |-> B ) /\ B <_ y ) -> E. z e. ran ( x e. A |-> B ) z <_ y )
16 12 13 15 syl2anc 
 |-  ( ( ph /\ x e. A /\ B <_ y ) -> E. z e. ran ( x e. A |-> B ) z <_ y )
17 16 3exp 
 |-  ( ph -> ( x e. A -> ( B <_ y -> E. z e. ran ( x e. A |-> B ) z <_ y ) ) )
18 1 7 17 rexlimd 
 |-  ( ph -> ( E. x e. A B <_ y -> E. z e. ran ( x e. A |-> B ) z <_ y ) )
19 nfv 
 |-  F/ z E. x e. A B <_ y
20 vex 
 |-  z e. _V
21 9 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B ) )
22 20 21 ax-mp 
 |-  ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B )
23 22 biimpi 
 |-  ( z e. ran ( x e. A |-> B ) -> E. x e. A z = B )
24 14 biimpcd 
 |-  ( z <_ y -> ( z = B -> B <_ y ) )
25 24 a1d 
 |-  ( z <_ y -> ( x e. A -> ( z = B -> B <_ y ) ) )
26 6 25 reximdai 
 |-  ( z <_ y -> ( E. x e. A z = B -> E. x e. A B <_ y ) )
27 26 com12 
 |-  ( E. x e. A z = B -> ( z <_ y -> E. x e. A B <_ y ) )
28 23 27 syl 
 |-  ( z e. ran ( x e. A |-> B ) -> ( z <_ y -> E. x e. A B <_ y ) )
29 19 28 rexlimi 
 |-  ( E. z e. ran ( x e. A |-> B ) z <_ y -> E. x e. A B <_ y )
30 29 a1i 
 |-  ( ph -> ( E. z e. ran ( x e. A |-> B ) z <_ y -> E. x e. A B <_ y ) )
31 18 30 impbid 
 |-  ( ph -> ( E. x e. A B <_ y <-> E. z e. ran ( x e. A |-> B ) z <_ y ) )
32 2 31 ralbid 
 |-  ( ph -> ( A. y e. RR E. x e. A B <_ y <-> A. y e. RR E. z e. ran ( x e. A |-> B ) z <_ y ) )
33 1 9 3 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR* )
34 infxrunb3 
 |-  ( ran ( x e. A |-> B ) C_ RR* -> ( A. y e. RR E. z e. ran ( x e. A |-> B ) z <_ y <-> inf ( ran ( x e. A |-> B ) , RR* , < ) = -oo ) )
35 33 34 syl 
 |-  ( ph -> ( A. y e. RR E. z e. ran ( x e. A |-> B ) z <_ y <-> inf ( ran ( x e. A |-> B ) , RR* , < ) = -oo ) )
36 32 35 bitrd 
 |-  ( ph -> ( A. y e. RR E. x e. A B <_ y <-> inf ( ran ( x e. A |-> B ) , RR* , < ) = -oo ) )