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 | ⊢ ran (,) ∈ TopBases |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ioof | ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ | |
| 2 | 1 | fdmi | ⊢ dom (,) = ( ℝ* × ℝ* ) |
| 3 | 2 | imaeq2i | ⊢ ( (,) “ dom (,) ) = ( (,) “ ( ℝ* × ℝ* ) ) |
| 4 | imadmrn | ⊢ ( (,) “ dom (,) ) = ran (,) | |
| 5 | 3 4 | eqtr3i | ⊢ ( (,) “ ( ℝ* × ℝ* ) ) = ran (,) |
| 6 | ssid | ⊢ ℝ* ⊆ ℝ* | |
| 7 | 6 | qtopbaslem | ⊢ ( (,) “ ( ℝ* × ℝ* ) ) ∈ TopBases |
| 8 | 5 7 | eqeltrri | ⊢ ran (,) ∈ TopBases |