Theorem tgioo 15655

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.)

Hypotheses

Ref	Expression
remet.1	⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))
tgioo.2	⊢ 𝐽 = (MetOpen‘𝐷)

Assertion

Ref	Expression
tgioo	⊢ (topGen‘ran (,)) = 𝐽

Proof of Theorem tgioo

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑎 𝑏 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		remet.1	. . . 4 ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))
2	1	rexmet 15650	. . 3 ⊢ 𝐷 ∈ (∞Met‘ℝ)
3		tgioo.2	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐷)
4	3	mopnval 15543	. . 3 ⊢ (𝐷 ∈ (∞Met‘ℝ) → 𝐽 = (topGen‘ran (ball‘𝐷)))
5	2, 4	ax-mp 5	. 2 ⊢ 𝐽 = (topGen‘ran (ball‘𝐷))
6		blex 15488	. . . . 5 ⊢ (𝐷 ∈ (∞Met‘ℝ) → (ball‘𝐷) ∈ V)
7	2, 6	ax-mp 5	. . . 4 ⊢ (ball‘𝐷) ∈ V
8	7	rnex 5050	. . 3 ⊢ ran (ball‘𝐷) ∈ V
9	1	blssioo 15654	. . 3 ⊢ ran (ball‘𝐷) ⊆ ran (,)
10		elssuni 3963	. . . . . . 7 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,))
11		unirnioo 10375	. . . . . . 7 ⊢ ℝ = ∪ ran (,)
12	10, 11	sseqtrrdi 3297	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ℝ)
13		retopbas 15624	. . . . . . . . . 10 ⊢ ran (,) ∈ TopBases
14	13	a1i 9	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ran (,) ∈ TopBases)
15		simpl 109	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ran (,))
16	12	sselda 3248	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ℝ)
17		1re 8325	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
18	1	bl2ioo 15651	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
19	17, 18	mpan2 429	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
20		peano2rem 8593	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ)
21	20	rexrd 8375	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ*)
22		peano2re 8462	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
23	22	rexrd 8375	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ*)
24		ioorebasg 10377	. . . . . . . . . . . 12 ⊢ (((𝑥 − 1) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*) → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
25	21, 23, 24	syl2anc 415	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
26	19, 25	eqeltrd 2315	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) ∈ ran (,))
27	16, 26	syl 14	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝐷)1) ∈ ran (,))
28		simpr 110	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣)
29		1rp 10058	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ+
30		blcntr 15517	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ ∧ 1 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
31	2, 29, 30	mp3an13 1369	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥(ball‘𝐷)1))
32	16, 31	syl 14	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
33	28, 32	elind 3414	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))
34		basis2 15149	. . . . . . . . 9 ⊢ (((ran (,) ∈ TopBases ∧ 𝑣 ∈ ran (,)) ∧ ((𝑥(ball‘𝐷)1) ∈ ran (,) ∧ 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
35	14, 15, 27, 33, 34	syl22anc 1279	. . . . . . . 8 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
36		ioof 10373	. . . . . . . . . . 11 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
37		ffn 5533	. . . . . . . . . . 11 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
38		ovelrn 6238	. . . . . . . . . . 11 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏)))
39	36, 37, 38	mp2b 8	. . . . . . . . . 10 ⊢ (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏))
40		eleq2 2302	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
41		sseq1 3271	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ↔ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
42	40, 41	anbi12d 477	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))))
43		inss2 3452	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)
44		sstr 3256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
45	43, 44	mpan2 429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
46	45	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
47		elioore 10314	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
48	47	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ ℝ)
49	48, 19	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
50	46, 49	sseqtrd 3286	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)))
51		dfss 3234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)) ↔ (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
52	50, 51	sylib 122	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
53		eliooxr 10329	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
54	21, 23	jca 306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*))
55	47, 54	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑥 − 1) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*))
56		iooinsup 12043	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑥 − 1) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*)) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )))
57	53, 55, 56	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )))
58	57	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )))
59	52, 58	eqtrd 2271	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )))
60		mnfxr 8382	. . . . . . . . . . . . . . . . . . . 20 ⊢ -∞ ∈ ℝ*
61	60	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ∈ ℝ*)
62	53	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
63	62	simpld 112	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑎 ∈ ℝ*)
64	48, 21	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ*)
65		xrmaxcl 12018	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℝ* ∧ (𝑥 − 1) ∈ ℝ*) → sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ*)
66	63, 64, 65	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ*)
67	62	simprd 114	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑏 ∈ ℝ*)
68	48, 22	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ)
69	68	rexrd 8375	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ*)
70		xrmincl 12032	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*) → inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ*)
71	67, 69, 70	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ*)
72	47, 20	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑥 − 1) ∈ ℝ)
73	72	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ)
74		mnflt 10185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 − 1) ∈ ℝ → -∞ < (𝑥 − 1))
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < (𝑥 − 1))
76		xrmax2sup 12020	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ℝ* ∧ (𝑥 − 1) ∈ ℝ*) → (𝑥 − 1) ≤ sup({𝑎, (𝑥 − 1)}, ℝ*, < ))
77	63, 64, 76	syl2anc 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ≤ sup({𝑎, (𝑥 − 1)}, ℝ*, < ))
78	61, 64, 66, 75, 77	xrltletrd 10213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < sup({𝑎, (𝑥 − 1)}, ℝ*, < ))
79		simpl 109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (𝑎(,)𝑏))
80	79, 59	eleqtrd 2317	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )))
81		eliooxr 10329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )) → (sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ* ∧ inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ*))
82		elex2 2838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )) → ∃𝑤 𝑤 ∈ (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )))
83		ioom 10695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ* ∧ inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ*) → (∃𝑤 𝑤 ∈ (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )) ↔ sup({𝑎, (𝑥 − 1)}, ℝ*, < ) < inf({𝑏, (𝑥 + 1)}, ℝ*, < )))
84	82, 83	imbitrid 154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ* ∧ inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ*) → (𝑥 ∈ (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )) → sup({𝑎, (𝑥 − 1)}, ℝ*, < ) < inf({𝑏, (𝑥 + 1)}, ℝ*, < )))
85	81, 84	mpcom 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )) → sup({𝑎, (𝑥 − 1)}, ℝ*, < ) < inf({𝑏, (𝑥 + 1)}, ℝ*, < ))
86	80, 85	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → sup({𝑎, (𝑥 − 1)}, ℝ*, < ) < inf({𝑏, (𝑥 + 1)}, ℝ*, < ))
87		xrre2 10223	. . . . . . . . . . . . . . . . . . 19 ⊢ (((-∞ ∈ ℝ* ∧ sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ* ∧ inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ*) ∧ (-∞ < sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∧ sup({𝑎, (𝑥 − 1)}, ℝ*, < ) < inf({𝑏, (𝑥 + 1)}, ℝ*, < ))) → sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ)
88	61, 66, 71, 78, 86, 87	syl32anc 1286	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ)
89		mnfle 10194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ* → -∞ ≤ sup({𝑎, (𝑥 − 1)}, ℝ*, < ))
90	66, 89	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ≤ sup({𝑎, (𝑥 − 1)}, ℝ*, < ))
91	61, 66, 71, 90, 86	xrlelttrd 10212	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < inf({𝑏, (𝑥 + 1)}, ℝ*, < ))
92		xrmin2inf 12034	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ*) → inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ≤ (𝑥 + 1))
93	67, 69, 92	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ≤ (𝑥 + 1))
94		xrre 10222	. . . . . . . . . . . . . . . . . . 19 ⊢ (((inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ* ∧ (𝑥 + 1) ∈ ℝ) ∧ (-∞ < inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∧ inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ≤ (𝑥 + 1))) → inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ)
95	71, 68, 91, 93, 94	syl22anc 1279	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ)
96	1	ioo2blex 15653	. . . . . . . . . . . . . . . . . 18 ⊢ ((sup({𝑎, (𝑥 − 1)}, ℝ*, < ) ∈ ℝ ∧ inf({𝑏, (𝑥 + 1)}, ℝ*, < ) ∈ ℝ) → (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )) ∈ ran (ball‘𝐷))
97	88, 95, 96	syl2anc 415	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (sup({𝑎, (𝑥 − 1)}, ℝ*, < )(,)inf({𝑏, (𝑥 + 1)}, ℝ*, < )) ∈ ran (ball‘𝐷))
98	59, 97	eqeltrd 2315	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ∈ ran (ball‘𝐷))
99		inss1 3451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣
100		sstr 3256	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣) → (𝑎(,)𝑏) ⊆ 𝑣)
101	99, 100	mpan2 429	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ 𝑣)
102	101	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ 𝑣)
103		sseq1 3271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ 𝑣 ↔ (𝑎(,)𝑏) ⊆ 𝑣))
104	40, 103	anbi12d 477	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)))
105	104	rspcev 2929	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎(,)𝑏) ∈ ran (ball‘𝐷) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
106	98, 79, 102, 105	syl12anc 1276	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
107		blssex 15531	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
108	2, 48, 107	sylancr 418	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
109	106, 108	mpbid 147	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
110	42, 109	biimtrdi 163	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
111	110	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*) → (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
112	111	rexlimivv 2674	. . . . . . . . . . 11 ⊢ (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
113	112	imp 124	. . . . . . . . . 10 ⊢ ((∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ* 𝑧 = (𝑎(,)𝑏) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
114	39, 113	sylanb 284	. . . . . . . . 9 ⊢ ((𝑧 ∈ ran (,) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
115	114	rexlimiva 2663	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
116	35, 115	syl 14	. . . . . . 7 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
117	116	ralrimiva 2623	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
118	3	elmopn2 15550	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘ℝ) → (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
119	2, 118	ax-mp 5	. . . . . 6 ⊢ (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
120	12, 117, 119	sylanbrc 421	. . . . 5 ⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ 𝐽)
121	120	ssriv 3252	. . . 4 ⊢ ran (,) ⊆ 𝐽
122	121, 5	sseqtri 3282	. . 3 ⊢ ran (,) ⊆ (topGen‘ran (ball‘𝐷))
123		2basgeng 15183	. . 3 ⊢ ((ran (ball‘𝐷) ∈ V ∧ ran (ball‘𝐷) ⊆ ran (,) ∧ ran (,) ⊆ (topGen‘ran (ball‘𝐷))) → (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,)))
124	8, 9, 122, 123	mp3an 1378	. 2 ⊢ (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,))
125	5, 124	eqtr2i 2260	1 ⊢ (topGen‘ran (,)) = 𝐽

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402  ∃wex 1545   ∈ wcel 2209  ∀wral 2528  ∃wrex 2529  Vcvv 2821   ∩ cin 3219   ⊆ wss 3220  𝒫 cpw 3688  {cpr 3710  ∪ cuni 3935   class class class wbr 4130   × cxp 4772  ran crn 4775   ↾ cres 4776   ∘ ccom 4778   Fn wfn 5372  ⟶wf 5373  ‘cfv 5377  (class class class)co 6085  supcsup 7322  infcinf 7323  ℝcr 8178  1c1 8180   + caddc 8182  -∞cmnf 8358  ℝ^*cxr 8359   < clt 8360   ≤ cle 8361   − cmin 8497  ℝ⁺crp 10054  (,)cioo 10290  abscabs 11763  topGenctg 13608  ∞Metcxmet 14873  ballcbl 14875  MetOpencmopn 14878  TopBasesctb 15143

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-mulrcl 8278  ax-addcom 8279  ax-mulcom 8280  ax-addass 8281  ax-mulass 8282  ax-distr 8283  ax-i2m1 8284  ax-0lt1 8285  ax-1rid 8286  ax-0id 8287  ax-rnegex 8288  ax-precex 8289  ax-cnre 8290  ax-pre-ltirr 8291  ax-pre-ltwlin 8292  ax-pre-lttrn 8293  ax-pre-apti 8294  ax-pre-ltadd 8295  ax-pre-mulgt0 8296  ax-pre-mulext 8297  ax-arch 8298  ax-caucvg 8299

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-isom 5386  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-recs 6576  df-frec 6662  df-map 6924  df-sup 7324  df-inf 7325  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-sub 8499  df-neg 8500  df-reap 8903  df-ap 8910  df-div 9003  df-inn 9305  df-2 9363  df-3 9364  df-4 9365  df-n0 9564  df-z 9645  df-uz 9922  df-q 10020  df-rp 10055  df-xneg 10174  df-xadd 10175  df-ioo 10294  df-seqfrec 10885  df-exp 10976  df-cj 11607  df-re 11608  df-im 11609  df-rsqrt 11764  df-abs 11765  df-topgen 13614  df-psmet 14880  df-xmet 14881  df-met 14882  df-bl 14883  df-mopn 14884  df-top 15099  df-bases 15144

This theorem is used by:  resubmet  15657  tgioo2cntop  15658  tgioo2  15660