tgqioo - Metamath Proof Explorer

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

Theorem tgqioo 21173

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 5354	. . 3
3		ioof 11634	. . . . . 6
4		ffn 5737	. . . . . 6
5	3, 4	ax-mp 5	. . . . 5
6		simpll 753	. . . . . . . . . 10 $/\$ $/\$
7		elioo1 11581	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
8	7	biimpa 484	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
9	8	simp1d 1008	. . . . . . . . . 10 $/\$ $/\$
10	8	simp2d 1009	. . . . . . . . . 10 $/\$ $/\$
11		qbtwnxr 11411	. . . . . . . . . 10 $/\$ $/\$ $/\$
12	6, 9, 10, 11	syl3anc 1228	. . . . . . . . 9 $/\$ $/\$ $/\$
13		simplr 754	. . . . . . . . . 10 $/\$ $/\$
14	8	simp3d 1010	. . . . . . . . . 10 $/\$ $/\$
15		qbtwnxr 11411	. . . . . . . . . 10 $/\$ $/\$ $/\$
16	9, 13, 14, 15	syl3anc 1228	. . . . . . . . 9 $/\$ $/\$ $/\$
17		reeanv 3034	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		df-ov 6298	. . . . . . . . . . . . . 14
19		opelxpi 5037	. . . . . . . . . . . . . . . 16 $/\$
20	19	3ad2ant2 1018	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		ffun 5739	. . . . . . . . . . . . . . . . 17
22	3, 21	ax-mp 5	. . . . . . . . . . . . . . . 16
23		qssre 11204	. . . . . . . . . . . . . . . . . . 19
24		ressxr 9649	. . . . . . . . . . . . . . . . . . 19
25	23, 24	sstri 3518	. . . . . . . . . . . . . . . . . 18
26		xpss12 5114	. . . . . . . . . . . . . . . . . 18 $/\$
27	25, 25, 26	mp2an 672	. . . . . . . . . . . . . . . . 17
28	3	fdmi 5742	. . . . . . . . . . . . . . . . 17
29	27, 28	sseqtr4i 3542	. . . . . . . . . . . . . . . 16
30		funfvima2 6147	. . . . . . . . . . . . . . . 16 $/\$
31	22, 29, 30	mp2an 672	. . . . . . . . . . . . . . 15
32	20, 31	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	18, 32	syl5eqel 2559	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	9	3ad2ant1 1017	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simp3lr 1068	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simp3rl 1069	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		simp2l 1022	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	25, 37	sseldi 3507	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		simp2r 1023	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	25, 39	sseldi 3507	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		elioo1 11581	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
42	38, 40, 41	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	34, 35, 36, 42	mpbir3and 1179	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	6	3ad2ant1 1017	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp3ll 1067	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46		xrltle 11367	. . . . . . . . . . . . . . . . 17 $/\$
47	44, 38, 46	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	45, 47	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		iooss1 11576	. . . . . . . . . . . . . . 15 $/\$
50	44, 48, 49	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	13	3ad2ant1 1017	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52		simp3rr 1070	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53		xrltle 11367	. . . . . . . . . . . . . . . . 17 $/\$
54	40, 51, 53	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	52, 54	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		iooss2 11577	. . . . . . . . . . . . . . 15 $/\$
57	51, 55, 56	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	50, 57	sstrd 3519	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		eleq2 2540	. . . . . . . . . . . . . . 15
60		sseq1 3530	. . . . . . . . . . . . . . 15
61	59, 60	anbi12d 710	. . . . . . . . . . . . . 14 $/\$ $/\$
62	61	rspcev 3219	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
63	33, 43, 58, 62	syl12anc 1226	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	63	3exp 1195	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	64	rexlimdvv 2965	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	17, 65	syl5bir 218	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	12, 16, 66	mp2and 679	. . . . . . . 8 $/\$ $/\$ $/\$
68	67	ralrimiva 2881	. . . . . . 7 $/\$ $/\$
69		qtopbas 21134	. . . . . . . 8
70		eltg2b 19329	. . . . . . . 8 $/\$
71	69, 70	ax-mp 5	. . . . . . 7 $/\$
72	68, 71	sylibr 212	. . . . . 6 $/\$
73	72	rgen2a 2894	. . . . 5
74		ffnov 6401	. . . . 5 $/\$
75	5, 73, 74	mpbir2an 918	. . . 4
76		frn 5743	. . . 4
77	75, 76	ax-mp 5	. . 3
78		2basgen 19360	. . 3 $/\$
79	2, 77, 78	mp2an 672	. 2
80	1, 79	eqtr2i 2497	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wcel 1767

wral 2817

wrex 2818

wss 3481

cpw 4016

cop 4039 class class class wbr 4453

cxp 5003

cdm 5005

crn 5006

cima 5008

wfun 5588

wfn 5589

wf 5590

cfv 5594 (class class class)co 6295

cr 9503

cxr 9639

clt 9640

cle 9641

cq 11194

cioo 11541

ctg 14710

ctb 19267

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587 ax-cnex 9560 ax-resscn 9561 ax-1cn 9562 ax-icn 9563 ax-addcl 9564 ax-addrcl 9565 ax-mulcl 9566 ax-mulrcl 9567 ax-mulcom 9568 ax-addass 9569 ax-mulass 9570 ax-distr 9571 ax-i2m1 9572 ax-1ne0 9573 ax-1rid 9574 ax-rnegex 9575 ax-rrecex 9576 ax-cnre 9577 ax-pre-lttri 9578 ax-pre-lttrn 9579 ax-pre-ltadd 9580 ax-pre-mulgt0 9581 ax-pre-sup 9582

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2822 df-rex 2823 df-reu 2824 df-rmo 2825 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-pss 3497 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-tp 4038 df-op 4040 df-uni 4252 df-iun 4333 df-br 4454 df-opab 4512 df-mpt 4513 df-tr 4547 df-eprel 4797 df-id 4801 df-po 4806 df-so 4807 df-fr 4844 df-we 4846 df-ord 4887 df-on 4888 df-lim 4889 df-suc 4890 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6256 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6696 df-1st 6795 df-2nd 6796 df-recs 7054 df-rdg 7088 df-er 7323 df-en 7529 df-dom 7530 df-sdom 7531 df-sup 7913 df-pnf 9642 df-mnf 9643 df-xr 9644 df-ltxr 9645 df-le 9646 df-sub 9819 df-neg 9820 df-div 10219 df-nn 10549 df-n0 10808 df-z 10877 df-uz 11095 df-q 11195 df-ioo 11545 df-topgen 14716 df-bases 19270

This theorem is referenced by: re2ndc 21174 opnmblALT 21880 mbfimaopnlem 21930

W3C validator