tgioo - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgioo		Structured version Visualization version GIF version

Theorem tgioo 24844

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 24839	. . 3 ⊢ 𝐷 ∈ (∞Met‘ℝ)
3		tgioo.2	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐷)
4	3	mopnval 24486	. . 3 ⊢ (𝐷 ∈ (∞Met‘ℝ) → 𝐽 = (topGen‘ran (ball‘𝐷)))
5	2, 4	ax-mp 5	. 2 ⊢ 𝐽 = (topGen‘ran (ball‘𝐷))
6	1	blssioo 24843	. . 3 ⊢ ran (ball‘𝐷) ⊆ ran (,)
7		elssuni 4894	. . . . . . 7 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,))
8		unirnioo 13447	. . . . . . 7 ⊢ ℝ = ∪ ran (,)
9	7, 8	sseqtrrdi 3975	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ℝ)
10		retopbas 24808	. . . . . . . . . 10 ⊢ ran (,) ∈ TopBases
11	10	a1i 11	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ran (,) ∈ TopBases)
12		simpl 486	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ran (,))
13	9	sselda 3934	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ℝ)
14		1re 11175	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
15	1	bl2ioo 24840	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
16	14, 15	mpan2 701	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
17		ioof 13445	. . . . . . . . . . . . 13 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
18		ffn 6686	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
19	17, 18	ax-mp 5	. . . . . . . . . . . 12 ⊢ (,) Fn (ℝ^* × ℝ^*)
20		peano2rem 11492	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ)
21	20	rexrd 11226	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ^*)
22		peano2re 11350	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
23	22	rexrd 11226	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ^*)
24		fnovrn 7566	. . . . . . . . . . . 12 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑥 − 1) ∈ ℝ^ ∧ (𝑥 + 1) ∈ ℝ^*) → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
25	19, 21, 23, 24	mp3an2i 1486	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
26	16, 25	eqeltrd 2861	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) ∈ ran (,))
27	13, 26	syl 17	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝐷)1) ∈ ran (,))
28		simpr 488	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣)
29		1rp 12991	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
30		blcntr 24461	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ ∧ 1 ∈ ℝ⁺) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
31	2, 29, 30	mp3an13 1472	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥(ball‘𝐷)1))
32	13, 31	syl 17	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
33	28, 32	elind 4150	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))
34		basis2 22999	. . . . . . . . 9 ⊢ (((ran (,) ∈ TopBases ∧ 𝑣 ∈ ran (,)) ∧ ((𝑥(ball‘𝐷)1) ∈ ran (,) ∧ 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
35	11, 12, 27, 33, 34	syl22anc 849	. . . . . . . 8 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
36		ovelrn 7567	. . . . . . . . . . 11 ⊢ ((,) Fn (ℝ^* × ℝ^) → (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏)))
37	19, 36	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏))
38		eleq2 2850	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
39		sseq1 3959	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ↔ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
40	38, 39	anbi12d 641	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))))
41		inss2 4187	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)
42		sstr 3942	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
43	41, 42	mpan2 701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
44	43	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
45		elioore 13373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
46	45	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ ℝ)
47	46, 16	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
48	44, 47	sseqtrd 3970	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)))
49		dfss 3921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)) ↔ (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
50	48, 49	sylib 220	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
51		eliooxr 13402	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*))
52	21, 23	jca 519	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*))
53	45, 52	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑥 − 1) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*))
54		iooin 13377	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑥 − 1) ∈ ℝ^ ∧ (𝑥 + 1) ∈ ℝ^*)) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
55	51, 53, 54	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
56	55	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
57	50, 56	eqtrd 2796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
58		mnfxr 11233	. . . . . . . . . . . . . . . . . . . 20 ⊢ -∞ ∈ ℝ^*
59	58	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ∈ ℝ^*)
60	46, 21	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ^*)
61	51	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*))
62	61	simpld 498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑎 ∈ ℝ^*)
63	60, 62	ifcld 4524	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^*)
64	61	simprd 499	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑏 ∈ ℝ^*)
65	46, 22	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ)
66	65	rexrd 11226	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ^*)
67	64, 66	ifcld 4524	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*)
68	45, 20	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑥 − 1) ∈ ℝ)
69	68	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ)
70	69	mnfltd 13120	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < (𝑥 − 1))
71		xrmax2 13173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ℝ^* ∧ (𝑥 − 1) ∈ ℝ^*) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
72	62, 60, 71	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
73	59, 60, 63, 70, 72	xrltletrd 13157	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
74		simpl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (𝑎(,)𝑏))
75	74, 57	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
76		eliooxr 13402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*))
77		ne0i 4291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅)
78		ioon0 13369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*) → ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅ ↔ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
79	77, 78	imbitrid 246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*) → (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
80	76, 79	mpcom 38	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
81	75, 80	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
82		xrre2 13167	. . . . . . . . . . . . . . . . . . 19 ⊢ (((-∞ ∈ ℝ^* ∧ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*) ∧ (-∞ < if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∧ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ)
83	59, 63, 67, 73, 81, 82	syl32anc 1396	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ)
84		mnfle 13131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* → -∞ ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
85	63, 84	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
86	59, 63, 67, 85, 81	xrlelttrd 13156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
87		xrmin2 13175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))
88	64, 66, 87	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))
89		xrre 13166	. . . . . . . . . . . . . . . . . . 19 ⊢ (((if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ) ∧ (-∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ)
90	67, 65, 86, 88, 89	syl22anc 849	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ)
91	1	ioo2blex 24842	. . . . . . . . . . . . . . . . . 18 ⊢ ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷))
92	83, 90, 91	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷))
93	57, 92	eqeltrd 2861	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ∈ ran (ball‘𝐷))
94		inss1 4186	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣
95		sstr 3942	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣) → (𝑎(,)𝑏) ⊆ 𝑣)
96	94, 95	mpan2 701	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ 𝑣)
97	96	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ 𝑣)
98		sseq1 3959	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ 𝑣 ↔ (𝑎(,)𝑏) ⊆ 𝑣))
99	38, 98	anbi12d 641	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)))
100	99	rspcev 3580	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎(,)𝑏) ∈ ran (ball‘𝐷) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
101	93, 74, 97, 100	syl12anc 847	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
102		blssex 24475	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
103	2, 46, 102	sylancr 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
104	101, 103	mpbid 234	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
105	40, 104	biimtrdi 255	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
106	105	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*) → (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
107	106	rexlimivv 3203	. . . . . . . . . . 11 ⊢ (∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
108	107	imp 410	. . . . . . . . . 10 ⊢ ((∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
109	37, 108	sylanb 590	. . . . . . . . 9 ⊢ ((𝑧 ∈ ran (,) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
110	109	rexlimiva 3154	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
111	35, 110	syl 17	. . . . . . 7 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
112	111	ralrimiva 3153	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
113	3	elmopn2 24493	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘ℝ) → (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
114	2, 113	ax-mp 5	. . . . . 6 ⊢ (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
115	9, 112, 114	sylanbrc 592	. . . . 5 ⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ 𝐽)
116	115	ssriv 3938	. . . 4 ⊢ ran (,) ⊆ 𝐽
117	116, 5	sseqtri 3982	. . 3 ⊢ ran (,) ⊆ (topGen‘ran (ball‘𝐷))
118		2basgen 23038	. . 3 ⊢ ((ran (ball‘𝐷) ⊆ ran (,) ∧ ran (,) ⊆ (topGen‘ran (ball‘𝐷))) → (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,)))
119	6, 117, 118	mp2an 702	. 2 ⊢ (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,))
120	5, 119	eqtr2i 2785	1 ⊢ (topGen‘ran (,)) = 𝐽

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∀wral 3075 ∃wrex 3085 ∩ cin 3901 ⊆ wss 3902 ∅c0 4283 ifcif 4477 𝒫 cpw 4552 ∪ cuni 4862 class class class wbr 5097 × cxp 5641 ran crn 5644 ↾ cres 5645 ∘ ccom 5647 Fn wfn 6511 ⟶wf 6512 ‘cfv 6516 (class class class)co 7391 ℝcr 11066 1c1 11068 + caddc 11070 -∞cmnf 11208 ℝ^*cxr 11209 < clt 11210 ≤ cle 11211 − cmin 11408 ℝ⁺crp 12987 (,)cioo 13343 abscabs 15252 topGenctg 17457 ∞Metcxmet 21397 ballcbl 21399 MetOpencmopn 21402 TopBasesctb 22993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-er 8672 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-sup 9382 df-inf 9383 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-n0 12476 df-z 12563 df-uz 12834 df-q 12944 df-rp 12988 df-xneg 13108 df-xadd 13109 df-xmul 13110 df-ioo 13347 df-seq 14009 df-exp 14069 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-topgen 17463 df-psmet 21404 df-xmet 21405 df-met 21406 df-bl 21407 df-mopn 21408 df-bases 22994

This theorem is referenced by: qdensere2 24845 rehaus 24847 resubmet 24850 tgioo2 24851 xrsmopn 24861 iccntr 24870 icccmplem3 24873 reconnlem2 24876 opnreen 24880 metdscn2 24906 evthicc 25509 opnmbllem 25651 dvlip2 26045 lhop 26066 dvcnvre 26069 nmcvcn 30855 opnrebl 36641 opnrebl2 36642 ptrecube 38080 poimirlem30 38110 opnmbllem0 38116 reheibor 38299

W3C validator