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 )