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 24695

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 13354	. . . . 5 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
2	1	fdmi 6670	. . . 4 ⊢ dom (,) = (ℝ^* × ℝ^*)
3	2	imaeq2i 6014	. . 3 ⊢ ((,) “ dom (,)) = ((,) “ (ℝ^* × ℝ^*))
4		imadmrn 6026	. . 3 ⊢ ((,) “ dom (,)) = ran (,)
5	3, 4	eqtr3i 2758	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) = ran (,)
6		ssid 3953	. . 3 ⊢ ℝ^* ⊆ ℝ^*
7	6	qtopbaslem 24693	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) ∈ TopBases
8	5, 7	eqeltrri 2830	1 ⊢ ran (,) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2113 𝒫 cpw 4551 × cxp 5619 dom cdm 5621 ran crn 5622 “ cima 5624 ℝcr 11016 ℝ^*cxr 11156 (,)cioo 13252 TopBasesctb 22880

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 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-cnex 11073 ax-resscn 11074 ax-pre-lttri 11091 ax-pre-lttrn 11092

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 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5516 df-po 5529 df-so 5530 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-ov 7358 df-oprab 7359 df-mpo 7360 df-1st 7930 df-2nd 7931 df-er 8631 df-en 8880 df-dom 8881 df-sdom 8882 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-ioo 13256 df-bases 22881

This theorem is referenced by: retop 24696 uniretop 24697 iooretop 24700 qdensere 24704 tgioo 24731 xrtgioo 24742 bndth 24904 ovolicc2 25470 cncombf 25606 cnmbf 25607 elmbfmvol2 34352 iccllysconn 35366 rellysconn 35367 mblfinlem3 37772 mblfinlem4 37773 ismblfin 37774 cnambfre 37781