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 24664

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 13368	. . . . 5 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
2	1	fdmi 6667	. . . 4 ⊢ dom (,) = (ℝ^* × ℝ^*)
3	2	imaeq2i 6013	. . 3 ⊢ ((,) “ dom (,)) = ((,) “ (ℝ^* × ℝ^*))
4		imadmrn 6025	. . 3 ⊢ ((,) “ dom (,)) = ran (,)
5	3, 4	eqtr3i 2754	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) = ran (,)
6		ssid 3960	. . 3 ⊢ ℝ^* ⊆ ℝ^*
7	6	qtopbaslem 24662	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) ∈ TopBases
8	5, 7	eqeltrri 2825	1 ⊢ ran (,) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2109 𝒫 cpw 4553 × cxp 5621 dom cdm 5623 ran crn 5624 “ cima 5626 ℝcr 11027 ℝ^*cxr 11167 (,)cioo 13266 TopBasesctb 22848

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-pre-lttri 11102 ax-pre-lttrn 11103

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 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-po 5531 df-so 5532 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-ov 7356 df-oprab 7357 df-mpo 7358 df-1st 7931 df-2nd 7932 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-ioo 13270 df-bases 22849

This theorem is referenced by: retop 24665 uniretop 24666 iooretop 24669 qdensere 24673 tgioo 24700 xrtgioo 24711 bndth 24873 ovolicc2 25439 cncombf 25575 cnmbf 25576 elmbfmvol2 34237 iccllysconn 35225 rellysconn 35226 mblfinlem3 37641 mblfinlem4 37642 ismblfin 37643 cnambfre 37650