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 24681

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 13353	. . . . 5 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
2	1	fdmi 6668	. . . 4 ⊢ dom (,) = (ℝ^* × ℝ^*)
3	2	imaeq2i 6012	. . 3 ⊢ ((,) “ dom (,)) = ((,) “ (ℝ^* × ℝ^*))
4		imadmrn 6024	. . 3 ⊢ ((,) “ dom (,)) = ran (,)
5	3, 4	eqtr3i 2756	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) = ran (,)
6		ssid 3952	. . 3 ⊢ ℝ^* ⊆ ℝ^*
7	6	qtopbaslem 24679	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) ∈ TopBases
8	5, 7	eqeltrri 2828	1 ⊢ ran (,) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2111 𝒫 cpw 4549 × cxp 5617 dom cdm 5619 ran crn 5620 “ cima 5622 ℝcr 11011 ℝ^*cxr 11151 (,)cioo 13251 TopBasesctb 22866

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 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11068 ax-resscn 11069 ax-pre-lttri 11086 ax-pre-lttrn 11087

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-id 5514 df-po 5527 df-so 5528 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-ov 7355 df-oprab 7356 df-mpo 7357 df-1st 7927 df-2nd 7928 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-pnf 11154 df-mnf 11155 df-xr 11156 df-ltxr 11157 df-le 11158 df-ioo 13255 df-bases 22867

This theorem is referenced by: retop 24682 uniretop 24683 iooretop 24686 qdensere 24690 tgioo 24717 xrtgioo 24728 bndth 24890 ovolicc2 25456 cncombf 25592 cnmbf 25593 elmbfmvol2 34287 iccllysconn 35301 rellysconn 35302 mblfinlem3 37705 mblfinlem4 37706 ismblfin 37707 cnambfre 37714