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 24022

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 13272	. . . . 5 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
2	1	fdmi 6657	. . . 4 ⊢ dom (,) = (ℝ^* × ℝ^*)
3	2	imaeq2i 5991	. . 3 ⊢ ((,) “ dom (,)) = ((,) “ (ℝ^* × ℝ^*))
4		imadmrn 6003	. . 3 ⊢ ((,) “ dom (,)) = ran (,)
5	3, 4	eqtr3i 2766	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) = ran (,)
6		ssid 3953	. . 3 ⊢ ℝ^* ⊆ ℝ^*
7	6	qtopbaslem 24020	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) ∈ TopBases
8	5, 7	eqeltrri 2834	1 ⊢ ran (,) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2105 𝒫 cpw 4546 × cxp 5612 dom cdm 5614 ran crn 5615 “ cima 5617 ℝcr 10963 ℝ^*cxr 11101 (,)cioo 13172 TopBasesctb 22193

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5240 ax-nul 5247 ax-pow 5305 ax-pr 5369 ax-un 7642 ax-cnex 11020 ax-resscn 11021 ax-pre-lttri 11038 ax-pre-lttrn 11039

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3404 df-v 3443 df-sbc 3727 df-csb 3843 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4269 df-if 4473 df-pw 4548 df-sn 4573 df-pr 4575 df-op 4579 df-uni 4852 df-iun 4940 df-br 5090 df-opab 5152 df-mpt 5173 df-id 5512 df-po 5526 df-so 5527 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6425 df-fun 6475 df-fn 6476 df-f 6477 df-f1 6478 df-fo 6479 df-f1o 6480 df-fv 6481 df-ov 7332 df-oprab 7333 df-mpo 7334 df-1st 7891 df-2nd 7892 df-er 8561 df-en 8797 df-dom 8798 df-sdom 8799 df-pnf 11104 df-mnf 11105 df-xr 11106 df-ltxr 11107 df-le 11108 df-ioo 13176 df-bases 22194

This theorem is referenced by: retop 24023 uniretop 24024 iooretop 24027 qdensere 24031 tgioo 24057 xrtgioo 24067 bndth 24219 ovolicc2 24784 cncombf 24920 cnmbf 24921 elmbfmvol2 32447 iccllysconn 33424 rellysconn 33425 mblfinlem3 35914 mblfinlem4 35915 ismblfin 35916 cnambfre 35923