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 24898

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 13475	. . . . 5 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
2	1	fdmi 6719	. . . 4 ⊢ dom (,) = (ℝ^* × ℝ^*)
3	2	imaeq2i 6062	. . 3 ⊢ ((,) “ dom (,)) = ((,) “ (ℝ^* × ℝ^*))
4		imadmrn 6074	. . 3 ⊢ ((,) “ dom (,)) = ran (,)
5	3, 4	eqtr3i 2788	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) = ran (,)
6		ssid 3960	. . 3 ⊢ ℝ^* ⊆ ℝ^*
7	6	qtopbaslem 24896	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) ∈ TopBases
8	5, 7	eqeltrri 2860	1 ⊢ ran (,) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2143 𝒫 cpw 4563 × cxp 5661 dom cdm 5663 ran crn 5664 “ cima 5666 ℝcr 11100 ℝ^*cxr 11243 (,)cioo 13373 TopBasesctb 23083

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-pre-lttri 11175 ax-pre-lttrn 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5558 df-po 5571 df-so 5572 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7415 df-oprab 7416 df-mpo 7417 df-1st 7987 df-2nd 7988 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-ioo 13377 df-bases 23084

This theorem is referenced by: retop 24899 uniretop 24900 iooretop 24903 qdensere 24907 tgioo 24934 xrtgioo 24945 bndth 25098 ovolicc2 25662 cncombf 25798 cnmbf 25799 elmbfmvol2 34638 iccllysconn 35723 rellysconn 35724 mblfinlem3 38291 mblfinlem4 38292 ismblfin 38293 cnambfre 38300