Theorem rellycmp

Description: The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	rellycmp

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
3	1	cnllycmp
4	1	recld2	$$⊢ℝ\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
5		cldllycmp
6	3 4 5	mp2an
7	2 6	eqeltri