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 )