Theorem retopbas

Description: A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007) (Proof shortened by Mario Carneiro, 17-Jun-2014)

	Ref	Expression
Assertion	retopbas	$$⊢\mathrm{ran}\left(.\right)\in \mathrm{TopBases}$$

Proof

Step	Hyp	Ref	Expression
1		ioof	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ$$
2	1	fdmi	$$⊢\mathrm{dom}\left(.\right)={ℝ}^{*}\times {ℝ}^{*}$$
3	2	imaeq2i	$$⊢\left(.\right)\left[\mathrm{dom}\left(.\right)\right]=\left(.\right)\left[{ℝ}^{*}\times {ℝ}^{*}\right]$$
4		imadmrn	$$⊢\left(.\right)\left[\mathrm{dom}\left(.\right)\right]=\mathrm{ran}\left(.\right)$$
5	3 4	eqtr3i	$$⊢\left(.\right)\left[{ℝ}^{*}\times {ℝ}^{*}\right]=\mathrm{ran}\left(.\right)$$
6		ssid	$$⊢{ℝ}^{*}\subseteq {ℝ}^{*}$$
7	6	qtopbaslem	$$⊢\left(.\right)\left[{ℝ}^{*}\times {ℝ}^{*}\right]\in \mathrm{TopBases}$$
8	5 7	eqeltrri	$$⊢\mathrm{ran}\left(.\right)\in \mathrm{TopBases}$$