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

Metamath Proof Explorer

Theorem infxrlbrnmpt2

Description: A member of a nonempty indexed set of reals is greater than or equal to the set's lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 infxrlbrnmpt2.x 
 |-  F/ x ph
2 infxrlbrnmpt2.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
3 infxrlbrnmpt2.c 
 |-  ( ph -> C e. A )
4 infxrlbrnmpt2.d 
 |-  ( ph -> D e. RR* )
5 infxrlbrnmpt2.e 
 |-  ( x = C -> B = D )
6 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
7 1 6 2 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR* )
8 6 5 elrnmpt1s 
 |-  ( ( C e. A /\ D e. RR* ) -> D e. ran ( x e. A |-> B ) )
9 3 4 8 syl2anc 
 |-  ( ph -> D e. ran ( x e. A |-> B ) )
10 infxrlb 
 |-  ( ( ran ( x e. A |-> B ) C_ RR* /\ D e. ran ( x e. A |-> B ) ) -> inf ( ran ( x e. A |-> B ) , RR* , < ) <_ D )
11 7 9 10 syl2anc 
 |-  ( ph -> inf ( ran ( x e. A |-> B ) , RR* , < ) <_ D )