tgqioo

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)

		Ref	Expression
	Hypothesis	tgqioo.1	$⊢ Q = topGen ((.) [ℚ \times ℚ])$
	Assertion	tgqioo	$⊢ topGen (ran (.)) = Q$

Proof

Step	Hyp	Ref	Expression
1		tgqioo.1	$⊢ Q = topGen ((.) [ℚ \times ℚ])$
2		imassrn	$⊢ (.) [ℚ \times ℚ] \subseteq ran (.)$
3		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
4		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
5	3 4	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
6		simpll	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to x \in ℝ^{*}$
7		elioo1	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (z \in (x, y) \leftrightarrow (z \in ℝ^{*} \land x < z \land z < y))$
8	7	biimpa	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to (z \in ℝ^{*} \land x < z \land z < y)$
9	8	simp1d	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to z \in ℝ^{*}$
10	8	simp2d	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to x < z$
11		qbtwnxr	$⊢ (x \in ℝ^{} \land z \in ℝ^{} \land x < z) \to \exists u \in ℚ (x < u \land u < z)$
12	6 9 10 11	syl3anc	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to \exists u \in ℚ (x < u \land u < z)$
13		simplr	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to y \in ℝ^{*}$
14	8	simp3d	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to z < y$
15		qbtwnxr	$⊢ (z \in ℝ^{} \land y \in ℝ^{} \land z < y) \to \exists v \in ℚ (z < v \land v < y)$
16	9 13 14 15	syl3anc	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to \exists v \in ℚ (z < v \land v < y)$
17		reeanv	$⊢ \exists u \in ℚ \exists v \in ℚ ((x < u \land u < z) \land (z < v \land v < y)) \leftrightarrow (\exists u \in ℚ (x < u \land u < z) \land \exists v \in ℚ (z < v \land v < y))$
18		df-ov	$⊢ (u, v) = (.) (⟨u, v⟩)$
19		opelxpi	$⊢ (u \in ℚ \land v \in ℚ) \to ⟨u, v⟩ \in (ℚ \times ℚ)$
20	19	3ad2ant2	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to ⟨u, v⟩ \in (ℚ \times ℚ)$
21		ffun	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to Fun (.)$
22	3 21	ax-mp	$⊢ Fun (.)$
23		qssre	$⊢ ℚ \subseteq ℝ$
24		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
25	23 24	sstri	$⊢ ℚ \subseteq ℝ^{*}$
26		xpss12	$⊢ (ℚ \subseteq ℝ^{} \land ℚ \subseteq ℝ^{}) \to ℚ \times ℚ \subseteq ℝ^{} \times ℝ^{}$
27	25 25 26	mp2an	$⊢ ℚ \times ℚ \subseteq ℝ^{} \times ℝ^{}$
28	3	fdmi	$⊢ dom (.) = ℝ^{} \times ℝ^{}$
29	27 28	sseqtrri	$⊢ ℚ \times ℚ \subseteq dom (.)$
30		funfvima2	$⊢ (Fun (.) \land ℚ \times ℚ \subseteq dom (.)) \to (⟨u, v⟩ \in (ℚ \times ℚ) \to (.) (⟨u, v⟩) \in (.) [ℚ \times ℚ])$
31	22 29 30	mp2an	$⊢ ⟨u, v⟩ \in (ℚ \times ℚ) \to (.) (⟨u, v⟩) \in (.) [ℚ \times ℚ]$
32	20 31	syl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to (.) (⟨u, v⟩) \in (.) [ℚ \times ℚ]$
33	18 32	eqeltrid	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to (u, v) \in (.) [ℚ \times ℚ]$
34	9	3ad2ant1	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to z \in ℝ^{*}$
35		simp3lr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to u < z$
36		simp3rl	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to z < v$
37		simp2l	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to u \in ℚ$
38	25 37	sseldi	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to u \in ℝ^{*}$
39		simp2r	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to v \in ℚ$
40	25 39	sseldi	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to v \in ℝ^{*}$
41		elioo1	$⊢ (u \in ℝ^{} \land v \in ℝ^{}) \to (z \in (u, v) \leftrightarrow (z \in ℝ^{*} \land u < z \land z < v))$
42	38 40 41	syl2anc	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to (z \in (u, v) \leftrightarrow (z \in ℝ^{*} \land u < z \land z < v))$
43	34 35 36 42	mpbir3and	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to z \in (u, v)$
44	6	3ad2ant1	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to x \in ℝ^{*}$
45		simp3ll	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to x < u$
46	44 38 45	xrltled	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to x \leq u$
47		iooss1	$⊢ (x \in ℝ^{*} \land x \leq u) \to (u, v) \subseteq (x, v)$
48	44 46 47	syl2anc	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to (u, v) \subseteq (x, v)$
49	13	3ad2ant1	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to y \in ℝ^{*}$
50		simp3rr	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to v < y$
51	40 49 50	xrltled	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to v \leq y$
52		iooss2	$⊢ (y \in ℝ^{*} \land v \leq y) \to (x, v) \subseteq (x, y)$
53	49 51 52	syl2anc	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to (x, v) \subseteq (x, y)$
54	48 53	sstrd	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to (u, v) \subseteq (x, y)$
55		eleq2	$⊢ w = (u, v) \to (z \in w \leftrightarrow z \in (u, v))$
56		sseq1	$⊢ w = (u, v) \to (w \subseteq (x, y) \leftrightarrow (u, v) \subseteq (x, y))$
57	55 56	anbi12d	$⊢ w = (u, v) \to ((z \in w \land w \subseteq (x, y)) \leftrightarrow (z \in (u, v) \land (u, v) \subseteq (x, y)))$
58	57	rspcev	$⊢ ((u, v) \in (.) [ℚ \times ℚ] \land (z \in (u, v) \land (u, v) \subseteq (x, y))) \to \exists w \in (.) [ℚ \times ℚ] (z \in w \land w \subseteq (x, y))$
59	33 43 54 58	syl12anc	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \land (u \in ℚ \land v \in ℚ) \land ((x < u \land u < z) \land (z < v \land v < y))) \to \exists w \in (.) [ℚ \times ℚ] (z \in w \land w \subseteq (x, y))$
60	59	3exp	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to ((u \in ℚ \land v \in ℚ) \to (((x < u \land u < z) \land (z < v \land v < y)) \to \exists w \in (.) [ℚ \times ℚ] (z \in w \land w \subseteq (x, y))))$
61	60	rexlimdvv	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to (\exists u \in ℚ \exists v \in ℚ ((x < u \land u < z) \land (z < v \land v < y)) \to \exists w \in (.) [ℚ \times ℚ] (z \in w \land w \subseteq (x, y)))$
62	17 61	syl5bir	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to ((\exists u \in ℚ (x < u \land u < z) \land \exists v \in ℚ (z < v \land v < y)) \to \exists w \in (.) [ℚ \times ℚ] (z \in w \land w \subseteq (x, y)))$
63	12 16 62	mp2and	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land z \in (x, y)) \to \exists w \in (.) [ℚ \times ℚ] (z \in w \land w \subseteq (x, y))$
64	63	ralrimiva	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to \forall z \in (x, y) \exists w \in (.) [ℚ \times ℚ] (z \in w \land w \subseteq (x, y))$
65		qtopbas	$⊢ (.) [ℚ \times ℚ] \in TopBases$
66		eltg2b	$⊢ (.) [ℚ \times ℚ] \in TopBases \to ((x, y) \in topGen ((.) [ℚ \times ℚ]) \leftrightarrow \forall z \in (x, y) \exists w \in (.) [ℚ \times ℚ] (z \in w \land w \subseteq (x, y)))$
67	65 66	ax-mp	$⊢ (x, y) \in topGen ((.) [ℚ \times ℚ]) \leftrightarrow \forall z \in (x, y) \exists w \in (.) [ℚ \times ℚ] (z \in w \land w \subseteq (x, y))$
68	64 67	sylibr	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x, y) \in topGen ((.) [ℚ \times ℚ])$
69	68	rgen2	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} (x, y) \in topGen ((.) [ℚ \times ℚ])$
70		ffnov	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ topGen ((.) [ℚ \times ℚ]) \leftrightarrow ((.) Fn (ℝ^{} \times ℝ^{}) \land \forall x \in ℝ^{} \forall y \in ℝ^{} (x, y) \in topGen ((.) [ℚ \times ℚ]))$
71	5 69 70	mpbir2an	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ topGen ((.) [ℚ \times ℚ])$
72		frn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ topGen ((.) [ℚ \times ℚ]) \to ran (.) \subseteq topGen ((.) [ℚ \times ℚ])$
73	71 72	ax-mp	$⊢ ran (.) \subseteq topGen ((.) [ℚ \times ℚ])$
74		2basgen	$⊢ ((.) [ℚ \times ℚ] \subseteq ran (.) \land ran (.) \subseteq topGen ((.) [ℚ \times ℚ])) \to topGen ((.) [ℚ \times ℚ]) = topGen (ran (.))$
75	2 73 74	mp2an	$⊢ topGen ((.) [ℚ \times ℚ]) = topGen (ran (.))$
76	1 75	eqtr2i	$⊢ topGen (ran (.)) = Q$

Metamath Proof Explorer

Theorem tgqioo

Proof