This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bilani 
 |-  ( ( ph /\ y e. ran ( x e. A |-> C ) ) -> E. x e. A y = C )
15 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
16 15 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
17 nfv 
 |-  F/ x z <_ y
18 16 17 nfrexw 
 |-  F/ x E. z e. ran ( x e. A |-> B ) z <_ y
19 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
20 7 elrnmpt1 
 |-  ( ( x e. A /\ B e. RR* ) -> B e. ran ( x e. A |-> B ) )
21 19 2 20 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
22 21 3adant3 
 |-  ( ( ph /\ x e. A /\ y = C ) -> B e. ran ( x e. A |-> B ) )
23 4 3adant3 
 |-  ( ( ph /\ x e. A /\ y = C ) -> B <_ C )
24 id 
 |-  ( y = C -> y = C )
25 24 eqcomd 
 |-  ( y = C -> C = y )
26 25 3ad2ant3 
 |-  ( ( ph /\ x e. A /\ y = C ) -> C = y )
27 23 26 breqtrd 
 |-  ( ( ph /\ x e. A /\ y = C ) -> B <_ y )
28 breq1 
 |-  ( z = B -> ( z <_ y <-> B <_ y ) )
29 28 rspcev 
 |-  ( ( B e. ran ( x e. A |-> B ) /\ B <_ y ) -> E. z e. ran ( x e. A |-> B ) z <_ y )
30 22 27 29 syl2anc 
 |-  ( ( ph /\ x e. A /\ y = C ) -> E. z e. ran ( x e. A |-> B ) z <_ y )
31 30 3exp 
 |-  ( ph -> ( x e. A -> ( y = C -> E. z e. ran ( x e. A |-> B ) z <_ y ) ) )
32 1 18 31 rexlimd 
 |-  ( ph -> ( E. x e. A y = C -> E. z e. ran ( x e. A |-> B ) z <_ y ) )
33 32 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 ) )
34 14 33 mpd 
 |-  ( ( ph /\ y e. ran ( x e. A |-> C ) ) -> E. z e. ran ( x e. A |-> B ) z <_ y )
35 5 6 8 10 34 infleinf2 
 |-  ( ph -> inf ( ran ( x e. A |-> B ) , RR* , < ) <_ inf ( ran ( x e. A |-> C ) , RR* , < ) )