# Metamath Proof Explorer

## Theorem icccmpALT

Description: A closed interval in RR is compact. Alternate proof of icccmp using the Heine-Borel theorem heibor . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Aug-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses icccmpALT.1 ${⊢}{J}=\left[{A},{B}\right]$
icccmpALT.2 ${⊢}{M}={\left(\mathrm{abs}\circ -\right)↾}_{\left({J}×{J}\right)}$
icccmpALT.3 ${⊢}{T}=\mathrm{MetOpen}\left({M}\right)$
Assertion icccmpALT ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {T}\in \mathrm{Comp}$

### Proof

Step Hyp Ref Expression
1 icccmpALT.1 ${⊢}{J}=\left[{A},{B}\right]$
2 icccmpALT.2 ${⊢}{M}={\left(\mathrm{abs}\circ -\right)↾}_{\left({J}×{J}\right)}$
3 icccmpALT.3 ${⊢}{T}=\mathrm{MetOpen}\left({M}\right)$
4 icccld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
5 1 4 eqeltrid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {J}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
6 1 2 iccbnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {M}\in \mathrm{Bnd}\left({J}\right)$
7 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
8 1 7 eqsstrid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {J}\subseteq ℝ$
9 eqid ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
10 2 3 9 reheibor ${⊢}{J}\subseteq ℝ\to \left({T}\in \mathrm{Comp}↔\left({J}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {M}\in \mathrm{Bnd}\left({J}\right)\right)\right)$
11 8 10 syl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({T}\in \mathrm{Comp}↔\left({J}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {M}\in \mathrm{Bnd}\left({J}\right)\right)\right)$
12 5 6 11 mpbir2and ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {T}\in \mathrm{Comp}$