Metamath Proof Explorer

Theorem infrnmptle

Description: An indexed infimum of extended reals is smaller than another indexed infimum of extended reals, when every indexed element is smaller than the corresponding one. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 infrnmptle.x 
 |-  F/ x ph
2 infrnmptle.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
3 infrnmptle.c 
 |-  ( ( ph /\ x e. A ) -> C e. RR* )
4 infrnmptle.l 
 |-  ( ( ph /\ x e. A ) -> B <_ C )
5 nfv 
 |-  F/ y ph
6 nfv 
 |-  F/ z ph
7 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
8 1 7 2 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR* )
9 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
10 1 9 3 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> C ) C_ RR* )
11 vex 
 |-  y e. _V
12 9 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( x e. A |-> C ) <-> E. x e. A y = C ) )
13 11 12 ax-mp 
 |-  ( y e. ran ( x e. A |-> C ) <-> E. x e. A y = C )
14 13 biimpi 
 |-  ( y e. ran ( x e. A |-> C ) -> E. x e. A y = C )
15 14 adantl 
 |-  ( ( ph /\ y e. ran ( x e. A |-> C ) ) -> E. x e. A y = C )
16 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
17 16 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
18 nfv 
 |-  F/ x z <_ y
19 17 18 nfrex 
 |-  F/ x E. z e. ran ( x e. A |-> B ) z <_ y
20 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
21 7 elrnmpt1 
 |-  ( ( x e. A /\ B e. RR* ) -> B e. ran ( x e. A |-> B ) )
22 20 2 21 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
23 22 3adant3 
 |-  ( ( ph /\ x e. A /\ y = C ) -> B e. ran ( x e. A |-> B ) )
24 4 3adant3 
 |-  ( ( ph /\ x e. A /\ y = C ) -> B <_ C )
25 id 
 |-  ( y = C -> y = C )
26 25 eqcomd 
 |-  ( y = C -> C = y )
27 26 3ad2ant3 
 |-  ( ( ph /\ x e. A /\ y = C ) -> C = y )
28 24 27 breqtrd 
 |-  ( ( ph /\ x e. A /\ y = C ) -> B <_ y )
29 breq1 
 |-  ( z = B -> ( z <_ y <-> B <_ y ) )
30 29 rspcev 
 |-  ( ( B e. ran ( x e. A |-> B ) /\ B <_ y ) -> E. z e. ran ( x e. A |-> B ) z <_ y )
31 23 28 30 syl2anc 
 |-  ( ( ph /\ x e. A /\ y = C ) -> E. z e. ran ( x e. A |-> B ) z <_ y )
32 31 3exp 
 |-  ( ph -> ( x e. A -> ( y = C -> E. z e. ran ( x e. A |-> B ) z <_ y ) ) )
33 1 19 32 rexlimd 
 |-  ( ph -> ( E. x e. A y = C -> E. z e. ran ( x e. A |-> B ) z <_ y ) )
34 33 adantr 
 |-  ( ( ph /\ y e. ran ( x e. A |-> C ) ) -> ( E. x e. A y = C -> E. z e. ran ( x e. A |-> B ) z <_ y ) )
35 15 34 mpd 
 |-  ( ( ph /\ y e. ran ( x e. A |-> C ) ) -> E. z e. ran ( x e. A |-> B ) z <_ y )
36 5 6 8 10 35 infleinf2 
 |-  ( ph -> inf ( ran ( x e. A |-> B ) , RR* , < ) <_ inf ( ran ( x e. A |-> C ) , RR* , < ) )