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* ) |
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* ) |