retopbas - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > retopbas		Structured version Visualization version GIF version

Theorem retopbas 24697

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

**Assertion**
Ref	Expression
retopbas	⊢ ran (,) ∈ TopBases

**Proof of Theorem retopbas**
Step	Hyp	Ref	Expression
1		ioof 13462	. . . . 5 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
2	1	fdmi 6716	. . . 4 ⊢ dom (,) = (ℝ^* × ℝ^*)
3	2	imaeq2i 6045	. . 3 ⊢ ((,) “ dom (,)) = ((,) “ (ℝ^* × ℝ^*))
4		imadmrn 6057	. . 3 ⊢ ((,) “ dom (,)) = ran (,)
5	3, 4	eqtr3i 2760	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) = ran (,)
6		ssid 3981	. . 3 ⊢ ℝ^* ⊆ ℝ^*
7	6	qtopbaslem 24695	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) ∈ TopBases
8	5, 7	eqeltrri 2831	1 ⊢ ran (,) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2108 𝒫 cpw 4575 × cxp 5652 dom cdm 5654 ran crn 5655 “ cima 5657 ℝcr 11126 ℝ^*cxr 11266 (,)cioo 13360 TopBasesctb 22881

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7727 ax-cnex 11183 ax-resscn 11184 ax-pre-lttri 11201 ax-pre-lttrn 11202

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-po 5561 df-so 5562 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-iota 6483 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537 df-fv 6538 df-ov 7406 df-oprab 7407 df-mpo 7408 df-1st 7986 df-2nd 7987 df-er 8717 df-en 8958 df-dom 8959 df-sdom 8960 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-ioo 13364 df-bases 22882

This theorem is referenced by: retop 24698 uniretop 24699 iooretop 24702 qdensere 24706 tgioo 24733 xrtgioo 24744 bndth 24906 ovolicc2 25473 cncombf 25609 cnmbf 25610 elmbfmvol2 34245 iccllysconn 35218 rellysconn 35219 mblfinlem3 37629 mblfinlem4 37630 ismblfin 37631 cnambfre 37638