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 24808

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 13445	. . . . 5 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
2	1	fdmi 6698	. . . 4 ⊢ dom (,) = (ℝ^* × ℝ^*)
3	2	imaeq2i 6043	. . 3 ⊢ ((,) “ dom (,)) = ((,) “ (ℝ^* × ℝ^*))
4		imadmrn 6055	. . 3 ⊢ ((,) “ dom (,)) = ran (,)
5	3, 4	eqtr3i 2786	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) = ran (,)
6		ssid 3956	. . 3 ⊢ ℝ^* ⊆ ℝ^*
7	6	qtopbaslem 24806	. 2 ⊢ ((,) “ (ℝ^* × ℝ^*)) ∈ TopBases
8	5, 7	eqeltrri 2858	1 ⊢ ran (,) ∈ TopBases

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2141 𝒫 cpw 4552 × cxp 5641 dom cdm 5643 ran crn 5644 “ cima 5646 ℝcr 11066 ℝ^*cxr 11209 (,)cioo 13343 TopBasesctb 22993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-pre-lttri 11141 ax-pre-lttrn 11142

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-id 5538 df-po 5551 df-so 5552 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-ov 7394 df-oprab 7395 df-mpo 7396 df-1st 7965 df-2nd 7966 df-er 8672 df-en 8922 df-dom 8923 df-sdom 8924 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-ioo 13347 df-bases 22994

This theorem is referenced by: retop 24809 uniretop 24810 iooretop 24813 qdensere 24817 tgioo 24844 xrtgioo 24855 bndth 25008 ovolicc2 25572 cncombf 25708 cnmbf 25709 elmbfmvol2 34525 iccllysconn 35561 rellysconn 35562 mblfinlem3 38119 mblfinlem4 38120 ismblfin 38121 cnambfre 38128