Metamath Proof Explorer


Theorem infxrrnmptcl

Description: The infimum of an arbitrary indexed set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses infxrrnmptcl.1
|- F/ x ph
infxrrnmptcl.2
|- ( ( ph /\ x e. A ) -> B e. RR* )
Assertion infxrrnmptcl
|- ( ph -> inf ( ran ( x e. A |-> B ) , RR* , < ) e. RR* )

Proof

Step Hyp Ref Expression
1 infxrrnmptcl.1
 |-  F/ x ph
2 infxrrnmptcl.2
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
3 eqid
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
4 1 3 2 rnmptssd
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR* )
5 4 infxrcld
 |-  ( ph -> inf ( ran ( x e. A |-> B ) , RR* , < ) e. RR* )