tgioo

Description: The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 13-Nov-2013)

	Ref	Expression
Hypotheses	remet.1	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
	tgioo.2	$⊢ J = MetOpen (D)$
Assertion	tgioo	$⊢ topGen (ran (.)) = J$

Proof

Step	Hyp	Ref	Expression
1		remet.1	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
2		tgioo.2	$⊢ J = MetOpen (D)$
3	1	rexmet	$⊢ D \in ∞Met (ℝ)$
4	2	mopnval	$⊢ D \in ∞Met (ℝ) \to J = topGen (ran ball (D))$
5	3 4	ax-mp	$⊢ J = topGen (ran ball (D))$
6	1	blssioo	$⊢ ran ball (D) \subseteq ran (.)$
7		elssuni	$⊢ v \in ran (.) \to v \subseteq ⋃ ran (.)$
8		unirnioo	$⊢ ℝ = ⋃ ran (.)$
9	7 8	sseqtrrdi	$⊢ v \in ran (.) \to v \subseteq ℝ$
10		retopbas	$⊢ ran (.) \in TopBases$
11	10	a1i	$⊢ (v \in ran (.) \land x \in v) \to ran (.) \in TopBases$
12		simpl	$⊢ (v \in ran (.) \land x \in v) \to v \in ran (.)$
13	9	sselda	$⊢ (v \in ran (.) \land x \in v) \to x \in ℝ$
14		1re	$⊢ 1 \in ℝ$
15	1	bl2ioo	$⊢ (x \in ℝ \land 1 \in ℝ) \to x ball (D) 1 = (x - 1, x + 1)$
16	14 15	mpan2	$⊢ x \in ℝ \to x ball (D) 1 = (x - 1, x + 1)$
17		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
18		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
19	17 18	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
20		peano2rem	$⊢ x \in ℝ \to x - 1 \in ℝ$
21	20	rexrd	$⊢ x \in ℝ \to x - 1 \in ℝ^{*}$
22		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
23	22	rexrd	$⊢ x \in ℝ \to x + 1 \in ℝ^{*}$
24		fnovrn	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land x - 1 \in ℝ^{} \land x + 1 \in ℝ^{}) \to (x - 1, x + 1) \in ran (.)$
25	19 21 23 24	mp3an2i	$⊢ x \in ℝ \to (x - 1, x + 1) \in ran (.)$
26	16 25	eqeltrd	$⊢ x \in ℝ \to x ball (D) 1 \in ran (.)$
27	13 26	syl	$⊢ (v \in ran (.) \land x \in v) \to x ball (D) 1 \in ran (.)$
28		simpr	$⊢ (v \in ran (.) \land x \in v) \to x \in v$
29		1rp	$⊢ 1 \in ℝ^{+}$
30		blcntr	$⊢ (D \in ∞Met (ℝ) \land x \in ℝ \land 1 \in ℝ^{+}) \to x \in (x ball (D) 1)$
31	3 29 30	mp3an13	$⊢ x \in ℝ \to x \in (x ball (D) 1)$
32	13 31	syl	$⊢ (v \in ran (.) \land x \in v) \to x \in (x ball (D) 1)$
33	28 32	elind	$⊢ (v \in ran (.) \land x \in v) \to x \in (v \cap (x ball (D) 1))$
34		basis2	$⊢ ((ran (.) \in TopBases \land v \in ran (.)) \land (x ball (D) 1 \in ran (.) \land x \in (v \cap (x ball (D) 1)))) \to \exists z \in ran (.) (x \in z \land z \subseteq v \cap (x ball (D) 1))$
35	11 12 27 33 34	syl22anc	$⊢ (v \in ran (.) \land x \in v) \to \exists z \in ran (.) (x \in z \land z \subseteq v \cap (x ball (D) 1))$
36		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (z \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b))$
37	19 36	ax-mp	$⊢ z \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b)$
38		eleq2	$⊢ z = (a, b) \to (x \in z \leftrightarrow x \in (a, b))$
39		sseq1	$⊢ z = (a, b) \to (z \subseteq v \cap (x ball (D) 1) \leftrightarrow (a, b) \subseteq v \cap (x ball (D) 1))$
40	38 39	anbi12d	$⊢ z = (a, b) \to ((x \in z \land z \subseteq v \cap (x ball (D) 1)) \leftrightarrow (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)))$
41		inss2	$⊢ v \cap (x ball (D) 1) \subseteq x ball (D) 1$
42		sstr	$⊢ ((a, b) \subseteq v \cap (x ball (D) 1) \land v \cap (x ball (D) 1) \subseteq x ball (D) 1) \to (a, b) \subseteq x ball (D) 1$
43	41 42	mpan2	$⊢ (a, b) \subseteq v \cap (x ball (D) 1) \to (a, b) \subseteq x ball (D) 1$
44	43	adantl	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (a, b) \subseteq x ball (D) 1$
45		elioore	$⊢ x \in (a, b) \to x \in ℝ$
46	45	adantr	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to x \in ℝ$
47	46 16	syl	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to x ball (D) 1 = (x - 1, x + 1)$
48	44 47	sseqtrd	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (a, b) \subseteq (x - 1, x + 1)$
49		dfss	$⊢ (a, b) \subseteq (x - 1, x + 1) \leftrightarrow (a, b) = (a, b) \cap (x - 1, x + 1)$
50	48 49	sylib	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (a, b) = (a, b) \cap (x - 1, x + 1)$
51		eliooxr	$⊢ x \in (a, b) \to (a \in ℝ^{} \land b \in ℝ^{})$
52	21 23	jca	$⊢ x \in ℝ \to (x - 1 \in ℝ^{} \land x + 1 \in ℝ^{})$
53	45 52	syl	$⊢ x \in (a, b) \to (x - 1 \in ℝ^{} \land x + 1 \in ℝ^{})$
54		iooin	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land (x - 1 \in ℝ^{} \land x + 1 \in ℝ^{})) \to (a, b) \cap (x - 1, x + 1) = (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1))$
55	51 53 54	syl2anc	$⊢ x \in (a, b) \to (a, b) \cap (x - 1, x + 1) = (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1))$
56	55	adantr	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (a, b) \cap (x - 1, x + 1) = (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1))$
57	50 56	eqtrd	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (a, b) = (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1))$
58		mnfxr	$⊢ −∞ \in ℝ^{*}$
59	58	a1i	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to −∞ \in ℝ^{*}$
60	46 21	syl	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to x - 1 \in ℝ^{*}$
61	51	adantr	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (a \in ℝ^{} \land b \in ℝ^{})$
62	61	simpld	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to a \in ℝ^{*}$
63	60 62	ifcld	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to if (a \leq x - 1, x - 1, a) \in ℝ^{*}$
64	61	simprd	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to b \in ℝ^{*}$
65	46 22	syl	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to x + 1 \in ℝ$
66	65	rexrd	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to x + 1 \in ℝ^{*}$
67	64 66	ifcld	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to if (b \leq x + 1, b, x + 1) \in ℝ^{*}$
68	45 20	syl	$⊢ x \in (a, b) \to x - 1 \in ℝ$
69	68	adantr	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to x - 1 \in ℝ$
70	69	mnfltd	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to −∞ < x - 1$
71		xrmax2	$⊢ (a \in ℝ^{} \land x - 1 \in ℝ^{}) \to x - 1 \leq if (a \leq x - 1, x - 1, a)$
72	62 60 71	syl2anc	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to x - 1 \leq if (a \leq x - 1, x - 1, a)$
73	59 60 63 70 72	xrltletrd	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to −∞ < if (a \leq x - 1, x - 1, a)$
74		simpl	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to x \in (a, b)$
75	74 57	eleqtrd	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to x \in (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1))$
76		eliooxr	$⊢ x \in (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1)) \to (if (a \leq x - 1, x - 1, a) \in ℝ^{} \land if (b \leq x + 1, b, x + 1) \in ℝ^{})$
77		ne0i	$⊢ x \in (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1)) \to (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1)) \neq \emptyset$
78		ioon0	$⊢ (if (a \leq x - 1, x - 1, a) \in ℝ^{} \land if (b \leq x + 1, b, x + 1) \in ℝ^{}) \to ((if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1)) \neq \emptyset \leftrightarrow if (a \leq x - 1, x - 1, a) < if (b \leq x + 1, b, x + 1))$
79	77 78	imbitrid	$⊢ (if (a \leq x - 1, x - 1, a) \in ℝ^{} \land if (b \leq x + 1, b, x + 1) \in ℝ^{}) \to (x \in (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1)) \to if (a \leq x - 1, x - 1, a) < if (b \leq x + 1, b, x + 1))$
80	76 79	mpcom	$⊢ x \in (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1)) \to if (a \leq x - 1, x - 1, a) < if (b \leq x + 1, b, x + 1)$
81	75 80	syl	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to if (a \leq x - 1, x - 1, a) < if (b \leq x + 1, b, x + 1)$
82		xrre2	$⊢ ((−∞ \in ℝ^{} \land if (a \leq x - 1, x - 1, a) \in ℝ^{} \land if (b \leq x + 1, b, x + 1) \in ℝ^{*}) \land (−∞ < if (a \leq x - 1, x - 1, a) \land if (a \leq x - 1, x - 1, a) < if (b \leq x + 1, b, x + 1))) \to if (a \leq x - 1, x - 1, a) \in ℝ$
83	59 63 67 73 81 82	syl32anc	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to if (a \leq x - 1, x - 1, a) \in ℝ$
84		mnfle	$⊢ if (a \leq x - 1, x - 1, a) \in ℝ^{*} \to −∞ \leq if (a \leq x - 1, x - 1, a)$
85	63 84	syl	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to −∞ \leq if (a \leq x - 1, x - 1, a)$
86	59 63 67 85 81	xrlelttrd	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to −∞ < if (b \leq x + 1, b, x + 1)$
87		xrmin2	$⊢ (b \in ℝ^{} \land x + 1 \in ℝ^{}) \to if (b \leq x + 1, b, x + 1) \leq x + 1$
88	64 66 87	syl2anc	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to if (b \leq x + 1, b, x + 1) \leq x + 1$
89		xrre	$⊢ ((if (b \leq x + 1, b, x + 1) \in ℝ^{*} \land x + 1 \in ℝ) \land (−∞ < if (b \leq x + 1, b, x + 1) \land if (b \leq x + 1, b, x + 1) \leq x + 1)) \to if (b \leq x + 1, b, x + 1) \in ℝ$
90	67 65 86 88 89	syl22anc	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to if (b \leq x + 1, b, x + 1) \in ℝ$
91	1	ioo2blex	$⊢ (if (a \leq x - 1, x - 1, a) \in ℝ \land if (b \leq x + 1, b, x + 1) \in ℝ) \to (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1)) \in ran ball (D)$
92	83 90 91	syl2anc	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (if (a \leq x - 1, x - 1, a), if (b \leq x + 1, b, x + 1)) \in ran ball (D)$
93	57 92	eqeltrd	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (a, b) \in ran ball (D)$
94		inss1	$⊢ v \cap (x ball (D) 1) \subseteq v$
95		sstr	$⊢ ((a, b) \subseteq v \cap (x ball (D) 1) \land v \cap (x ball (D) 1) \subseteq v) \to (a, b) \subseteq v$
96	94 95	mpan2	$⊢ (a, b) \subseteq v \cap (x ball (D) 1) \to (a, b) \subseteq v$
97	96	adantl	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (a, b) \subseteq v$
98		sseq1	$⊢ z = (a, b) \to (z \subseteq v \leftrightarrow (a, b) \subseteq v)$
99	38 98	anbi12d	$⊢ z = (a, b) \to ((x \in z \land z \subseteq v) \leftrightarrow (x \in (a, b) \land (a, b) \subseteq v))$
100	99	rspcev	$⊢ ((a, b) \in ran ball (D) \land (x \in (a, b) \land (a, b) \subseteq v)) \to \exists z \in ran ball (D) (x \in z \land z \subseteq v)$
101	93 74 97 100	syl12anc	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to \exists z \in ran ball (D) (x \in z \land z \subseteq v)$
102		blssex	$⊢ (D \in ∞Met (ℝ) \land x \in ℝ) \to (\exists z \in ran ball (D) (x \in z \land z \subseteq v) \leftrightarrow \exists y \in ℝ^{+} x ball (D) y \subseteq v)$
103	3 46 102	sylancr	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to (\exists z \in ran ball (D) (x \in z \land z \subseteq v) \leftrightarrow \exists y \in ℝ^{+} x ball (D) y \subseteq v)$
104	101 103	mpbid	$⊢ (x \in (a, b) \land (a, b) \subseteq v \cap (x ball (D) 1)) \to \exists y \in ℝ^{+} x ball (D) y \subseteq v$
105	40 104	syl6bi	$⊢ z = (a, b) \to ((x \in z \land z \subseteq v \cap (x ball (D) 1)) \to \exists y \in ℝ^{+} x ball (D) y \subseteq v)$
106	105	a1i	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (z = (a, b) \to ((x \in z \land z \subseteq v \cap (x ball (D) 1)) \to \exists y \in ℝ^{+} x ball (D) y \subseteq v))$
107	106	rexlimivv	$⊢ \exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b) \to ((x \in z \land z \subseteq v \cap (x ball (D) 1)) \to \exists y \in ℝ^{+} x ball (D) y \subseteq v)$
108	107	imp	$⊢ (\exists a \in ℝ^{} \exists b \in ℝ^{} z = (a, b) \land (x \in z \land z \subseteq v \cap (x ball (D) 1))) \to \exists y \in ℝ^{+} x ball (D) y \subseteq v$
109	37 108	sylanb	$⊢ (z \in ran (.) \land (x \in z \land z \subseteq v \cap (x ball (D) 1))) \to \exists y \in ℝ^{+} x ball (D) y \subseteq v$
110	109	rexlimiva	$⊢ \exists z \in ran (.) (x \in z \land z \subseteq v \cap (x ball (D) 1)) \to \exists y \in ℝ^{+} x ball (D) y \subseteq v$
111	35 110	syl	$⊢ (v \in ran (.) \land x \in v) \to \exists y \in ℝ^{+} x ball (D) y \subseteq v$
112	111	ralrimiva	$⊢ v \in ran (.) \to \forall x \in v \exists y \in ℝ^{+} x ball (D) y \subseteq v$
113	2	elmopn2	$⊢ D \in ∞Met (ℝ) \to (v \in J \leftrightarrow (v \subseteq ℝ \land \forall x \in v \exists y \in ℝ^{+} x ball (D) y \subseteq v))$
114	3 113	ax-mp	$⊢ v \in J \leftrightarrow (v \subseteq ℝ \land \forall x \in v \exists y \in ℝ^{+} x ball (D) y \subseteq v)$
115	9 112 114	sylanbrc	$⊢ v \in ran (.) \to v \in J$
116	115	ssriv	$⊢ ran (.) \subseteq J$
117	116 5	sseqtri	$⊢ ran (.) \subseteq topGen (ran ball (D))$
118		2basgen	$⊢ (ran ball (D) \subseteq ran (.) \land ran (.) \subseteq topGen (ran ball (D))) \to topGen (ran ball (D)) = topGen (ran (.))$
119	6 117 118	mp2an	$⊢ topGen (ran ball (D)) = topGen (ran (.))$
120	5 119	eqtr2i	$⊢ topGen (ran (.)) = J$

Metamath Proof Explorer

Theorem tgioo

Proof