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 24882

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 13470	. . . . 5 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
2	1	fdmi 6715	. . . 4 ⊢ dom (,) = (ℝ^* × ℝ^*)
3	2	imaeq2i 6058	. . 3 ⊢ ((,) “ dom (,)) = ((,) “ (ℝ^* × ℝ^*))
4		imadmrn 6070	. . 3 ⊢ ((,) “ dom (,)) = ran (,)
5	3, 4	eqtr3i 2794	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) = ran (,)
6		ssid 3967	. . 3 ⊢ ℝ^* ⊆ ℝ^*
7	6	qtopbaslem 24880	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) ∈ TopBases
8	5, 7	eqeltrri 2866	1 ⊢ ran (,) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2149 𝒫 cpw 4564 × cxp 5657 dom cdm 5659 ran crn 5660 “ cima 5662 ℝcr 11095 ℝ^*cxr 11238 (,)cioo 13368 TopBasesctb 23067

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-cnex 11152 ax-resscn 11153 ax-pre-lttri 11170 ax-pre-lttrn 11171

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5554 df-po 5567 df-so 5568 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7411 df-oprab 7412 df-mpo 7413 df-1st 7982 df-2nd 7983 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11241 df-mnf 11242 df-xr 11243 df-ltxr 11244 df-le 11245 df-ioo 13372 df-bases 23068

This theorem is referenced by: retop 24883 uniretop 24884 iooretop 24887 qdensere 24891 tgioo 24918 xrtgioo 24929 bndth 25082 ovolicc2 25646 cncombf 25782 cnmbf 25783 elmbfmvol2 34598 iccllysconn 35637 rellysconn 35638 mblfinlem3 38193 mblfinlem4 38194 ismblfin 38195 cnambfre 38202