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 24660

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 24655	. . 3 ⊢ 𝐷 ∈ (∞Met‘ℝ)
3		tgioo.2	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐷)
4	3	mopnval 24302	. . 3 ⊢ (𝐷 ∈ (∞Met‘ℝ) → 𝐽 = (topGen‘ran (ball‘𝐷)))
5	2, 4	ax-mp 5	. 2 ⊢ 𝐽 = (topGen‘ran (ball‘𝐷))
6	1	blssioo 24659	. . 3 ⊢ ran (ball‘𝐷) ⊆ ran (,)
7		elssuni 4897	. . . . . . 7 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,))
8		unirnioo 13386	. . . . . . 7 ⊢ ℝ = ∪ ran (,)
9	7, 8	sseqtrrdi 3985	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ℝ)
10		retopbas 24624	. . . . . . . . . 10 ⊢ ran (,) ∈ TopBases
11	10	a1i 11	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ran (,) ∈ TopBases)
12		simpl 482	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ran (,))
13	9	sselda 3943	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ℝ)
14		1re 11150	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
15	1	bl2ioo 24656	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
16	14, 15	mpan2 691	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
17		ioof 13384	. . . . . . . . . . . . 13 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
18		ffn 6670	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
19	17, 18	ax-mp 5	. . . . . . . . . . . 12 ⊢ (,) Fn (ℝ^* × ℝ^*)
20		peano2rem 11465	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ)
21	20	rexrd 11200	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ^*)
22		peano2re 11323	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
23	22	rexrd 11200	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ^*)
24		fnovrn 7544	. . . . . . . . . . . 12 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑥 − 1) ∈ ℝ^ ∧ (𝑥 + 1) ∈ ℝ^*) → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
25	19, 21, 23, 24	mp3an2i 1468	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
26	16, 25	eqeltrd 2828	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) ∈ ran (,))
27	13, 26	syl 17	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝐷)1) ∈ ran (,))
28		simpr 484	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣)
29		1rp 12931	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
30		blcntr 24277	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ ∧ 1 ∈ ℝ⁺) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
31	2, 29, 30	mp3an13 1454	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥(ball‘𝐷)1))
32	13, 31	syl 17	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
33	28, 32	elind 4159	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))
34		basis2 22814	. . . . . . . . 9 ⊢ (((ran (,) ∈ TopBases ∧ 𝑣 ∈ ran (,)) ∧ ((𝑥(ball‘𝐷)1) ∈ ran (,) ∧ 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
35	11, 12, 27, 33, 34	syl22anc 838	. . . . . . . 8 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
36		ovelrn 7545	. . . . . . . . . . 11 ⊢ ((,) Fn (ℝ^* × ℝ^) → (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏)))
37	19, 36	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏))
38		eleq2 2817	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
39		sseq1 3969	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ↔ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
40	38, 39	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))))
41		inss2 4197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)
42		sstr 3952	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
43	41, 42	mpan2 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
44	43	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
45		elioore 13312	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
46	45	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ ℝ)
47	46, 16	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
48	44, 47	sseqtrd 3980	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)))
49		dfss 3930	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)) ↔ (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
50	48, 49	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
51		eliooxr 13341	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*))
52	21, 23	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*))
53	45, 52	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑥 − 1) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*))
54		iooin 13316	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑥 − 1) ∈ ℝ^ ∧ (𝑥 + 1) ∈ ℝ^*)) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
55	51, 53, 54	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
56	55	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
57	50, 56	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
58		mnfxr 11207	. . . . . . . . . . . . . . . . . . . 20 ⊢ -∞ ∈ ℝ^*
59	58	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ∈ ℝ^*)
60	46, 21	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ^*)
61	51	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*))
62	61	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑎 ∈ ℝ^*)
63	60, 62	ifcld 4531	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^*)
64	61	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑏 ∈ ℝ^*)
65	46, 22	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ)
66	65	rexrd 11200	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ^*)
67	64, 66	ifcld 4531	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*)
68	45, 20	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑥 − 1) ∈ ℝ)
69	68	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ)
70	69	mnfltd 13060	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < (𝑥 − 1))
71		xrmax2 13112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ℝ^* ∧ (𝑥 − 1) ∈ ℝ^*) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
72	62, 60, 71	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
73	59, 60, 63, 70, 72	xrltletrd 13097	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
74		simpl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (𝑎(,)𝑏))
75	74, 57	eleqtrd 2830	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
76		eliooxr 13341	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*))
77		ne0i 4300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅)
78		ioon0 13308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*) → ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅ ↔ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
79	77, 78	imbitrid 244	. . . . . . . . . . . . . . . . . . . . 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 13106	. . . . . . . . . . . . . . . . . . 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 1380	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ)
84		mnfle 13071	. . . . . . . . . . . . . . . . . . . . 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 13096	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
87		xrmin2 13114	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))
88	64, 66, 87	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))
89		xrre 13105	. . . . . . . . . . . . . . . . . . 19 ⊢ (((if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ) ∧ (-∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ)
90	67, 65, 86, 88, 89	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ)
91	1	ioo2blex 24658	. . . . . . . . . . . . . . . . . 18 ⊢ ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷))
92	83, 90, 91	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷))
93	57, 92	eqeltrd 2828	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ∈ ran (ball‘𝐷))
94		inss1 4196	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣
95		sstr 3952	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣) → (𝑎(,)𝑏) ⊆ 𝑣)
96	94, 95	mpan2 691	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ 𝑣)
97	96	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ 𝑣)
98		sseq1 3969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ 𝑣 ↔ (𝑎(,)𝑏) ⊆ 𝑣))
99	38, 98	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)))
100	99	rspcev 3585	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎(,)𝑏) ∈ ran (ball‘𝐷) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
101	93, 74, 97, 100	syl12anc 836	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
102		blssex 24291	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
103	2, 46, 102	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
104	101, 103	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
105	40, 104	biimtrdi 253	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
106	105	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*) → (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
107	106	rexlimivv 3177	. . . . . . . . . . 11 ⊢ (∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
108	107	imp 406	. . . . . . . . . 10 ⊢ ((∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
109	37, 108	sylanb 581	. . . . . . . . 9 ⊢ ((𝑧 ∈ ran (,) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
110	109	rexlimiva 3126	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
111	35, 110	syl 17	. . . . . . 7 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
112	111	ralrimiva 3125	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
113	3	elmopn2 24309	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘ℝ) → (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
114	2, 113	ax-mp 5	. . . . . 6 ⊢ (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
115	9, 112, 114	sylanbrc 583	. . . . 5 ⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ 𝐽)
116	115	ssriv 3947	. . . 4 ⊢ ran (,) ⊆ 𝐽
117	116, 5	sseqtri 3992	. . 3 ⊢ ran (,) ⊆ (topGen‘ran (ball‘𝐷))
118		2basgen 22853	. . 3 ⊢ ((ran (ball‘𝐷) ⊆ ran (,) ∧ ran (,) ⊆ (topGen‘ran (ball‘𝐷))) → (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,)))
119	6, 117, 118	mp2an 692	. 2 ⊢ (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,))
120	5, 119	eqtr2i 2753	1 ⊢ (topGen‘ran (,)) = 𝐽

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 ∩ cin 3910 ⊆ wss 3911 ∅c0 4292 ifcif 4484 𝒫 cpw 4559 ∪ cuni 4867 class class class wbr 5102 × cxp 5629 ran crn 5632 ↾ cres 5633 ∘ ccom 5635 Fn wfn 6494 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 ℝcr 11043 1c1 11045 + caddc 11047 -∞cmnf 11182 ℝ^*cxr 11183 < clt 11184 ≤ cle 11185 − cmin 11381 ℝ⁺crp 12927 (,)cioo 13282 abscabs 15176 topGenctg 17376 ∞Metcxmet 21225 ballcbl 21227 MetOpencmopn 21230 TopBasesctb 22808

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-sup 9369 df-inf 9370 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-z 12506 df-uz 12770 df-q 12884 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-ioo 13286 df-seq 13943 df-exp 14003 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-topgen 17382 df-psmet 21232 df-xmet 21233 df-met 21234 df-bl 21235 df-mopn 21236 df-bases 22809

This theorem is referenced by: qdensere2 24661 rehaus 24663 resubmet 24666 tgioo2 24667 xrsmopn 24677 iccntr 24686 icccmplem3 24689 reconnlem2 24692 opnreen 24696 metdscn2 24722 evthicc 25336 opnmbllem 25478 dvlip2 25876 lhop 25897 dvcnvre 25900 nmcvcn 30597 opnrebl 36281 opnrebl2 36282 ptrecube 37587 poimirlem30 37617 opnmbllem0 37623 reheibor 37806

W3C validator