tgqioo - Metamath Proof Explorer

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

Theorem tgqioo 21390

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 5260	. . 3
3		ioof 11543	. . . . . 6
4		ffn 5639	. . . . . 6
5	3, 4	ax-mp 5	. . . . 5
6		simpll 751	. . . . . . . . . 10 $/\$ $/\$
7		elioo1 11490	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
8	7	biimpa 482	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
9	8	simp1d 1006	. . . . . . . . . 10 $/\$ $/\$
10	8	simp2d 1007	. . . . . . . . . 10 $/\$ $/\$
11		qbtwnxr 11320	. . . . . . . . . 10 $/\$ $/\$ $/\$
12	6, 9, 10, 11	syl3anc 1226	. . . . . . . . 9 $/\$ $/\$ $/\$
13		simplr 753	. . . . . . . . . 10 $/\$ $/\$
14	8	simp3d 1008	. . . . . . . . . 10 $/\$ $/\$
15		qbtwnxr 11320	. . . . . . . . . 10 $/\$ $/\$ $/\$
16	9, 13, 14, 15	syl3anc 1226	. . . . . . . . 9 $/\$ $/\$ $/\$
17		reeanv 2950	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		df-ov 6199	. . . . . . . . . . . . . 14
19		opelxpi 4945	. . . . . . . . . . . . . . . 16 $/\$
20	19	3ad2ant2 1016	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		ffun 5641	. . . . . . . . . . . . . . . . 17
22	3, 21	ax-mp 5	. . . . . . . . . . . . . . . 16
23		qssre 11111	. . . . . . . . . . . . . . . . . . 19
24		ressxr 9548	. . . . . . . . . . . . . . . . . . 19
25	23, 24	sstri 3426	. . . . . . . . . . . . . . . . . 18
26		xpss12 5021	. . . . . . . . . . . . . . . . . 18 $/\$
27	25, 25, 26	mp2an 670	. . . . . . . . . . . . . . . . 17
28	3	fdmi 5644	. . . . . . . . . . . . . . . . 17
29	27, 28	sseqtr4i 3450	. . . . . . . . . . . . . . . 16
30		funfvima2 6049	. . . . . . . . . . . . . . . 16 $/\$
31	22, 29, 30	mp2an 670	. . . . . . . . . . . . . . 15
32	20, 31	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	18, 32	syl5eqel 2474	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	9	3ad2ant1 1015	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simp3lr 1066	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simp3rl 1067	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		simp2l 1020	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	25, 37	sseldi 3415	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		simp2r 1021	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	25, 39	sseldi 3415	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		elioo1 11490	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
42	38, 40, 41	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	34, 35, 36, 42	mpbir3and 1177	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	6	3ad2ant1 1015	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp3ll 1065	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46		xrltle 11276	. . . . . . . . . . . . . . . . 17 $/\$
47	44, 38, 46	syl2anc 659	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	45, 47	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		iooss1 11485	. . . . . . . . . . . . . . 15 $/\$
50	44, 48, 49	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	13	3ad2ant1 1015	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52		simp3rr 1068	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53		xrltle 11276	. . . . . . . . . . . . . . . . 17 $/\$
54	40, 51, 53	syl2anc 659	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	52, 54	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		iooss2 11486	. . . . . . . . . . . . . . 15 $/\$
57	51, 55, 56	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	50, 57	sstrd 3427	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		eleq2 2455	. . . . . . . . . . . . . . 15
60		sseq1 3438	. . . . . . . . . . . . . . 15
61	59, 60	anbi12d 708	. . . . . . . . . . . . . 14 $/\$ $/\$
62	61	rspcev 3135	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
63	33, 43, 58, 62	syl12anc 1224	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	63	3exp 1193	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	64	rexlimdvv 2880	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	17, 65	syl5bir 218	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	12, 16, 66	mp2and 677	. . . . . . . 8 $/\$ $/\$ $/\$
68	67	ralrimiva 2796	. . . . . . 7 $/\$ $/\$
69		qtopbas 21351	. . . . . . . 8
70		eltg2b 19545	. . . . . . . 8 $/\$
71	69, 70	ax-mp 5	. . . . . . 7 $/\$
72	68, 71	sylibr 212	. . . . . 6 $/\$
73	72	rgen2a 2809	. . . . 5
74		ffnov 6305	. . . . 5 $/\$
75	5, 73, 74	mpbir2an 918	. . . 4
76		frn 5645	. . . 4
77	75, 76	ax-mp 5	. . 3
78		2basgen 19577	. . 3 $/\$
79	2, 77, 78	mp2an 670	. 2
80	1, 79	eqtr2i 2412	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826

wral 2732

wrex 2733

wss 3389

cpw 3927

cop 3950 class class class wbr 4367

cxp 4911

cdm 4913

crn 4914

cima 4916

wfun 5490

wfn 5491

wf 5492

cfv 5496 (class class class)co 6196

cr 9402

cxr 9538

clt 9539

cle 9540

cq 11101

cioo 11450

ctg 14845

ctb 19483

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480 ax-pre-sup 9481

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-1st 6699 df-2nd 6700 df-recs 6960 df-rdg 6994 df-er 7229 df-en 7436 df-dom 7437 df-sdom 7438 df-sup 7816 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-n0 10713 df-z 10782 df-uz 11002 df-q 11102 df-ioo 11454 df-topgen 14851 df-bases 19486

This theorem is referenced by: re2ndc 21391 opnmblALT 22097 mbfimaopnlem 22147

W3C validator