tgqioo - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgqioo		Structured version Unicode version

Theorem tgqioo 20376

Description: The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014.)

**Hypothesis**
Ref	Expression
tgqioo.1

**Assertion**
Ref	Expression
tgqioo

Proof of Theorem tgqioo Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tgqioo.1	. 2
2		imassrn 5179	. . 3
3		ioof 11386	. . . . . 6
4		ffn 5558	. . . . . 6
5	3, 4	ax-mp 5	. . . . 5
6		simpll 753	. . . . . . . . . 10 $/\$ $/\$
7		elioo1 11339	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
8	7	biimpa 484	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
9	8	simp1d 1000	. . . . . . . . . 10 $/\$ $/\$
10	8	simp2d 1001	. . . . . . . . . 10 $/\$ $/\$
11		qbtwnxr 11169	. . . . . . . . . 10 $/\$ $/\$ $/\$
12	6, 9, 10, 11	syl3anc 1218	. . . . . . . . 9 $/\$ $/\$ $/\$
13		simplr 754	. . . . . . . . . 10 $/\$ $/\$
14	8	simp3d 1002	. . . . . . . . . 10 $/\$ $/\$
15		qbtwnxr 11169	. . . . . . . . . 10 $/\$ $/\$ $/\$
16	9, 13, 14, 15	syl3anc 1218	. . . . . . . . 9 $/\$ $/\$ $/\$
17		reeanv 2887	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		df-ov 6093	. . . . . . . . . . . . . 14
19		opelxpi 4870	. . . . . . . . . . . . . . . 16 $/\$
20	19	3ad2ant2 1010	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		ffun 5560	. . . . . . . . . . . . . . . . 17
22	3, 21	ax-mp 5	. . . . . . . . . . . . . . . 16
23		qssre 10962	. . . . . . . . . . . . . . . . . . 19
24		ressxr 9426	. . . . . . . . . . . . . . . . . . 19
25	23, 24	sstri 3364	. . . . . . . . . . . . . . . . . 18
26		xpss12 4944	. . . . . . . . . . . . . . . . . 18 $/\$
27	25, 25, 26	mp2an 672	. . . . . . . . . . . . . . . . 17
28	3	fdmi 5563	. . . . . . . . . . . . . . . . 17
29	27, 28	sseqtr4i 3388	. . . . . . . . . . . . . . . 16
30		funfvima2 5952	. . . . . . . . . . . . . . . 16 $/\$
31	22, 29, 30	mp2an 672	. . . . . . . . . . . . . . 15
32	20, 31	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	18, 32	syl5eqel 2526	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	9	3ad2ant1 1009	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simp3lr 1060	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simp3rl 1061	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		simp2l 1014	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	25, 37	sseldi 3353	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		simp2r 1015	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	25, 39	sseldi 3353	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		elioo1 11339	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
42	38, 40, 41	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	34, 35, 36, 42	mpbir3and 1171	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	6	3ad2ant1 1009	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp3ll 1059	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46		xrltle 11125	. . . . . . . . . . . . . . . . 17 $/\$
47	44, 38, 46	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	45, 47	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		iooss1 11334	. . . . . . . . . . . . . . 15 $/\$
50	44, 48, 49	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	13	3ad2ant1 1009	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52		simp3rr 1062	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53		xrltle 11125	. . . . . . . . . . . . . . . . 17 $/\$
54	40, 51, 53	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	52, 54	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		iooss2 11335	. . . . . . . . . . . . . . 15 $/\$
57	51, 55, 56	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	50, 57	sstrd 3365	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		eleq2 2503	. . . . . . . . . . . . . . 15
60		sseq1 3376	. . . . . . . . . . . . . . 15
61	59, 60	anbi12d 710	. . . . . . . . . . . . . 14 $/\$ $/\$
62	61	rspcev 3072	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
63	33, 43, 58, 62	syl12anc 1216	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	63	3exp 1186	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	64	rexlimdvv 2846	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	17, 65	syl5bir 218	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	12, 16, 66	mp2and 679	. . . . . . . 8 $/\$ $/\$ $/\$
68	67	ralrimiva 2798	. . . . . . 7 $/\$ $/\$
69		qtopbas 20337	. . . . . . . 8
70		eltg2b 18563	. . . . . . . 8 $/\$
71	69, 70	ax-mp 5	. . . . . . 7 $/\$
72	68, 71	sylibr 212	. . . . . 6 $/\$
73	72	rgen2a 2781	. . . . 5
74		ffnov 6193	. . . . 5 $/\$
75	5, 73, 74	mpbir2an 911	. . . 4
76		frn 5564	. . . 4
77	75, 76	ax-mp 5	. . 3
78		2basgen 18594	. . 3 $/\$
79	2, 77, 78	mp2an 672	. 2
80	1, 79	eqtr2i 2463	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

wral 2714

wrex 2715

wss 3327

cpw 3859

cop 3882 class class class wbr 4291

cxp 4837

cdm 4839

crn 4840

cima 4842

wfun 5411

wfn 5412

wf 5413

cfv 5417 (class class class)co 6090

cr 9280

cxr 9416

clt 9417

cle 9418

cq 10952

cioo 11299

ctg 14375

ctb 18501

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4412 ax-nul 4420 ax-pow 4469 ax-pr 4530 ax-un 6371 ax-cnex 9337 ax-resscn 9338 ax-1cn 9339 ax-icn 9340 ax-addcl 9341 ax-addrcl 9342 ax-mulcl 9343 ax-mulrcl 9344 ax-mulcom 9345 ax-addass 9346 ax-mulass 9347 ax-distr 9348 ax-i2m1 9349 ax-1ne0 9350 ax-1rid 9351 ax-rnegex 9352 ax-rrecex 9353 ax-cnre 9354 ax-pre-lttri 9355 ax-pre-lttrn 9356 ax-pre-ltadd 9357 ax-pre-mulgt0 9358 ax-pre-sup 9359

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2567 df-ne 2607 df-nel 2608 df-ral 2719 df-rex 2720 df-reu 2721 df-rmo 2722 df-rab 2723 df-v 2973 df-sbc 3186 df-csb 3288 df-dif 3330 df-un 3332 df-in 3334 df-ss 3341 df-pss 3343 df-nul 3637 df-if 3791 df-pw 3861 df-sn 3877 df-pr 3879 df-tp 3881 df-op 3883 df-uni 4091 df-iun 4172 df-br 4292 df-opab 4350 df-mpt 4351 df-tr 4385 df-eprel 4631 df-id 4635 df-po 4640 df-so 4641 df-fr 4678 df-we 4680 df-ord 4721 df-on 4722 df-lim 4723 df-suc 4724 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5380 df-fun 5419 df-fn 5420 df-f 5421 df-f1 5422 df-fo 5423 df-f1o 5424 df-fv 5425 df-riota 6051 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6831 df-rdg 6865 df-er 7100 df-en 7310 df-dom 7311 df-sdom 7312 df-sup 7690 df-pnf 9419 df-mnf 9420 df-xr 9421 df-ltxr 9422 df-le 9423 df-sub 9596 df-neg 9597 df-div 9993 df-nn 10322 df-n0 10579 df-z 10646 df-uz 10861 df-q 10953 df-ioo 11303 df-topgen 14381 df-bases 18504

This theorem is referenced by: re2ndc 20377 opnmblALT 21082 mbfimaopnlem 21132

W3C validator