tgqioo - Metamath Proof Explorer

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

Theorem tgqioo 21175

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 5335	. . 3
3		ioof 11628	. . . . . 6
4		ffn 5718	. . . . . 6
5	3, 4	ax-mp 5	. . . . 5
6		simpll 753	. . . . . . . . . 10 $/\$ $/\$
7		elioo1 11575	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
8	7	biimpa 484	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
9	8	simp1d 1007	. . . . . . . . . 10 $/\$ $/\$
10	8	simp2d 1008	. . . . . . . . . 10 $/\$ $/\$
11		qbtwnxr 11405	. . . . . . . . . 10 $/\$ $/\$ $/\$
12	6, 9, 10, 11	syl3anc 1227	. . . . . . . . 9 $/\$ $/\$ $/\$
13		simplr 754	. . . . . . . . . 10 $/\$ $/\$
14	8	simp3d 1009	. . . . . . . . . 10 $/\$ $/\$
15		qbtwnxr 11405	. . . . . . . . . 10 $/\$ $/\$ $/\$
16	9, 13, 14, 15	syl3anc 1227	. . . . . . . . 9 $/\$ $/\$ $/\$
17		reeanv 3009	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		df-ov 6281	. . . . . . . . . . . . . 14
19		opelxpi 5018	. . . . . . . . . . . . . . . 16 $/\$
20	19	3ad2ant2 1017	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		ffun 5720	. . . . . . . . . . . . . . . . 17
22	3, 21	ax-mp 5	. . . . . . . . . . . . . . . 16
23		qssre 11198	. . . . . . . . . . . . . . . . . . 19
24		ressxr 9637	. . . . . . . . . . . . . . . . . . 19
25	23, 24	sstri 3496	. . . . . . . . . . . . . . . . . 18
26		xpss12 5095	. . . . . . . . . . . . . . . . . 18 $/\$
27	25, 25, 26	mp2an 672	. . . . . . . . . . . . . . . . 17
28	3	fdmi 5723	. . . . . . . . . . . . . . . . 17
29	27, 28	sseqtr4i 3520	. . . . . . . . . . . . . . . 16
30		funfvima2 6130	. . . . . . . . . . . . . . . 16 $/\$
31	22, 29, 30	mp2an 672	. . . . . . . . . . . . . . 15
32	20, 31	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	18, 32	syl5eqel 2533	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	9	3ad2ant1 1016	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simp3lr 1067	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simp3rl 1068	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		simp2l 1021	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	25, 37	sseldi 3485	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		simp2r 1022	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	25, 39	sseldi 3485	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		elioo1 11575	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
42	38, 40, 41	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	34, 35, 36, 42	mpbir3and 1178	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	6	3ad2ant1 1016	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp3ll 1066	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46		xrltle 11361	. . . . . . . . . . . . . . . . 17 $/\$
47	44, 38, 46	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	45, 47	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		iooss1 11570	. . . . . . . . . . . . . . 15 $/\$
50	44, 48, 49	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	13	3ad2ant1 1016	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52		simp3rr 1069	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53		xrltle 11361	. . . . . . . . . . . . . . . . 17 $/\$
54	40, 51, 53	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	52, 54	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		iooss2 11571	. . . . . . . . . . . . . . 15 $/\$
57	51, 55, 56	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	50, 57	sstrd 3497	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		eleq2 2514	. . . . . . . . . . . . . . 15
60		sseq1 3508	. . . . . . . . . . . . . . 15
61	59, 60	anbi12d 710	. . . . . . . . . . . . . 14 $/\$ $/\$
62	61	rspcev 3194	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
63	33, 43, 58, 62	syl12anc 1225	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	63	3exp 1194	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	64	rexlimdvv 2939	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	17, 65	syl5bir 218	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	12, 16, 66	mp2and 679	. . . . . . . 8 $/\$ $/\$ $/\$
68	67	ralrimiva 2855	. . . . . . 7 $/\$ $/\$
69		qtopbas 21136	. . . . . . . 8
70		eltg2b 19330	. . . . . . . 8 $/\$
71	69, 70	ax-mp 5	. . . . . . 7 $/\$
72	68, 71	sylibr 212	. . . . . 6 $/\$
73	72	rgen2a 2868	. . . . 5
74		ffnov 6388	. . . . 5 $/\$
75	5, 73, 74	mpbir2an 918	. . . 4
76		frn 5724	. . . 4
77	75, 76	ax-mp 5	. . 3
78		2basgen 19362	. . 3 $/\$
79	2, 77, 78	mp2an 672	. 2
80	1, 79	eqtr2i 2471	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1381

wcel 1802

wral 2791

wrex 2792

wss 3459

cpw 3994

cop 4017 class class class wbr 4434

cxp 4984

cdm 4986

crn 4987

cima 4989

wfun 5569

wfn 5570

wf 5571

cfv 5575 (class class class)co 6278

cr 9491

cxr 9627

clt 9628

cle 9629

cq 11188

cioo 11535

ctg 14709

ctb 19268

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-sep 4555 ax-nul 4563 ax-pow 4612 ax-pr 4673 ax-un 6574 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3419 df-dif 3462 df-un 3464 df-in 3466 df-ss 3473 df-pss 3475 df-nul 3769 df-if 3924 df-pw 3996 df-sn 4012 df-pr 4014 df-tp 4016 df-op 4018 df-uni 4232 df-iun 4314 df-br 4435 df-opab 4493 df-mpt 4494 df-tr 4528 df-eprel 4778 df-id 4782 df-po 4787 df-so 4788 df-fr 4825 df-we 4827 df-ord 4868 df-on 4869 df-lim 4870 df-suc 4871 df-xp 4992 df-rel 4993 df-cnv 4994 df-co 4995 df-dm 4996 df-rn 4997 df-res 4998 df-ima 4999 df-iota 5538 df-fun 5577 df-fn 5578 df-f 5579 df-f1 5580 df-fo 5581 df-f1o 5582 df-fv 5583 df-riota 6239 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-om 6683 df-1st 6782 df-2nd 6783 df-recs 7041 df-rdg 7075 df-er 7310 df-en 7516 df-dom 7517 df-sdom 7518 df-sup 7900 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9809 df-neg 9810 df-div 10210 df-nn 10540 df-n0 10799 df-z 10868 df-uz 11088 df-q 11189 df-ioo 11539 df-topgen 14715 df-bases 19271

This theorem is referenced by: re2ndc 21176 opnmblALT 21882 mbfimaopnlem 21932

W3C validator