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)\upharpoonright }_{\left(J\times 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)\upharpoonright }_{\left(J\times 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}\leftrightarrow \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}\leftrightarrow \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}$$