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 25022

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 25017	. . 3 ⊢ 𝐷 ∈ (∞Met‘ℝ)
3		tgioo.2	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐷)
4	3	mopnval 24664	. . 3 ⊢ (𝐷 ∈ (∞Met‘ℝ) → 𝐽 = (topGen‘ran (ball‘𝐷)))
5	2, 4	ax-mp 5	. 2 ⊢ 𝐽 = (topGen‘ran (ball‘𝐷))
6	1	blssioo 25021	. . 3 ⊢ ran (ball‘𝐷) ⊆ ran (,)
7		elssuni 4899	. . . . . . 7 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,))
8		unirnioo 13502	. . . . . . 7 ⊢ ℝ = ∪ ran (,)
9	7, 8	sseqtrrdi 3972	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ℝ)
10		retopbas 24986	. . . . . . . . . 10 ⊢ ran (,) ∈ TopBases
11	10	a1i 11	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ran (,) ∈ TopBases)
12		simpl 488	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ran (,))
13	9	sselda 3931	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ℝ)
14		1re 11232	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
15	1	bl2ioo 25018	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
16	14, 15	mpan2 704	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
17		ioof 13500	. . . . . . . . . . . . 13 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
18		ffn 6702	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
19	17, 18	ax-mp 5	. . . . . . . . . . . 12 ⊢ (,) Fn (ℝ^* × ℝ^*)
20		peano2rem 11549	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ)
21	20	rexrd 11283	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ^*)
22		peano2re 11407	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
23	22	rexrd 11283	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ^*)
24		fnovrn 7589	. . . . . . . . . . . 12 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑥 − 1) ∈ ℝ^ ∧ (𝑥 + 1) ∈ ℝ^*) → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
25	19, 21, 23, 24	mp3an2i 1495	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
26	16, 25	eqeltrd 2860	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) ∈ ran (,))
27	13, 26	syl 18	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝐷)1) ∈ ran (,))
28		simpr 490	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣)
29		1rp 13046	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
30		blcntr 24639	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ ∧ 1 ∈ ℝ⁺) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
31	2, 29, 30	mp3an13 1481	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥(ball‘𝐷)1))
32	13, 31	syl 18	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
33	28, 32	elind 4146	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))
34		basis2 23176	. . . . . . . . 9 ⊢ (((ran (,) ∈ TopBases ∧ 𝑣 ∈ ran (,)) ∧ ((𝑥(ball‘𝐷)1) ∈ ran (,) ∧ 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
35	11, 12, 27, 33, 34	syl22anc 852	. . . . . . . 8 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
36		ovelrn 7590	. . . . . . . . . . 11 ⊢ ((,) Fn (ℝ^* × ℝ^) → (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏)))
37	19, 36	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏))
38		eleq2 2849	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
39		sseq1 3956	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ↔ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
40	38, 39	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))))
41		inss2 4183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)
42		sstr 3939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
43	41, 42	mpan2 704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
44	43	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ (𝑥(ball‘𝐷)1))
45		elioore 13428	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
46	45	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ ℝ)
47	46, 16	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
48	44, 47	sseqtrd 3967	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)))
49		dfss 3918	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)) ↔ (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
50	48, 49	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
51		eliooxr 13457	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*))
52	21, 23	jca 521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*))
53	45, 52	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑥 − 1) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*))
54		iooin 13432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^) ∧ ((𝑥 − 1) ∈ ℝ^ ∧ (𝑥 + 1) ∈ ℝ^*)) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
55	51, 53, 54	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
56	55	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
57	50, 56	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
58		mnfxr 11290	. . . . . . . . . . . . . . . . . . . 20 ⊢ -∞ ∈ ℝ^*
59	58	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ∈ ℝ^*)
60	46, 21	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ^*)
61	51	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*))
62	61	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑎 ∈ ℝ^*)
63	60, 62	ifcld 4529	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^*)
64	61	simprd 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑏 ∈ ℝ^*)
65	46, 22	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ)
66	65	rexrd 11283	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ^*)
67	64, 66	ifcld 4529	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*)
68	45, 20	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑥 − 1) ∈ ℝ)
69	68	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ)
70	69	mnfltd 13175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < (𝑥 − 1))
71		xrmax2 13228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ℝ^* ∧ (𝑥 − 1) ∈ ℝ^*) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
72	62, 60, 71	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
73	59, 60, 63, 70, 72	xrltletrd 13212	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
74		simpl 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (𝑎(,)𝑏))
75	74, 57	eleqtrd 2862	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
76		eliooxr 13457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*))
77		ne0i 4287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅)
78		ioon0 13424	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*) → ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅ ↔ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
79	77, 78	imbitrid 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*) → (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
80	76, 79	mpcom 39	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
81	75, 80	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
82		xrre2 13222	. . . . . . . . . . . . . . . . . . 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 1405	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ)
84		mnfle 13186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* → -∞ ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
85	63, 84	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ ≤ if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
86	59, 63, 67, 85, 81	xrlelttrd 13211	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
87		xrmin2 13230	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))
88	64, 66, 87	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))
89		xrre 13221	. . . . . . . . . . . . . . . . . . 19 ⊢ (((if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ) ∧ (-∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ)
90	67, 65, 86, 88, 89	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ)
91	1	ioo2blex 25020	. . . . . . . . . . . . . . . . . 18 ⊢ ((if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷))
92	83, 90, 91	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ∈ ran (ball‘𝐷))
93	57, 92	eqeltrd 2860	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ∈ ran (ball‘𝐷))
94		inss1 4182	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣
95		sstr 3939	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣) → (𝑎(,)𝑏) ⊆ 𝑣)
96	94, 95	mpan2 704	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ 𝑣)
97	96	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ 𝑣)
98		sseq1 3956	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ 𝑣 ↔ (𝑎(,)𝑏) ⊆ 𝑣))
99	38, 98	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)))
100	99	rspcev 3576	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎(,)𝑏) ∈ ran (ball‘𝐷) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
101	93, 74, 97, 100	syl12anc 850	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
102		blssex 24653	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
103	2, 46, 102	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
104	101, 103	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
105	40, 104	biimtrdi 256	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
106	105	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*) → (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
107	106	rexlimivv 3204	. . . . . . . . . . 11 ⊢ (∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
108	107	imp 412	. . . . . . . . . 10 ⊢ ((∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
109	37, 108	sylanb 593	. . . . . . . . 9 ⊢ ((𝑧 ∈ ran (,) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
110	109	rexlimiva 3155	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
111	35, 110	syl 18	. . . . . . 7 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
112	111	ralrimiva 3154	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
113	3	elmopn2 24671	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘ℝ) → (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
114	2, 113	ax-mp 5	. . . . . 6 ⊢ (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
115	9, 112, 114	sylanbrc 595	. . . . 5 ⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ 𝐽)
116	115	ssriv 3935	. . . 4 ⊢ ran (,) ⊆ 𝐽
117	116, 5	sseqtri 3979	. . 3 ⊢ ran (,) ⊆ (topGen‘ran (ball‘𝐷))
118		2basgen 23215	. . 3 ⊢ ((ran (ball‘𝐷) ⊆ ran (,) ∧ ran (,) ⊆ (topGen‘ran (ball‘𝐷))) → (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,)))
119	6, 117, 118	mp2an 705	. 2 ⊢ (topGen‘ran (ball‘𝐷)) = (topGen‘ran (,))
120	5, 119	eqtr2i 2784	1 ⊢ (topGen‘ran (,)) = 𝐽

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 ifcif 4482 𝒫 cpw 4557 ∪ cuni 4867 class class class wbr 5103 × cxp 5653 ran crn 5656 ↾ cres 5657 ∘ ccom 5659 Fn wfn 6528 ⟶wf 6529 ‘cfv 6533 (class class class)co 7413 ℝcr 11123 1c1 11125 + caddc 11127 -∞cmnf 11265 ℝ^*cxr 11266 < clt 11267 ≤ cle 11268 − cmin 11465 ℝ⁺crp 13042 (,)cioo 13398 abscabs 15321 topGenctg 17522 ∞Metcxmet 21570 ballcbl 21572 MetOpencmopn 21575 TopBasesctb 23170

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201 ax-pre-sup 11202

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-er 8696 df-map 8828 df-en 8953 df-dom 8954 df-sdom 8955 df-sup 9412 df-inf 9413 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11467 df-neg 11468 df-div 11896 df-nn 12258 df-2 12327 df-3 12328 df-n0 12529 df-z 12616 df-uz 12888 df-q 12998 df-rp 13043 df-xneg 13163 df-xadd 13164 df-xmul 13165 df-ioo 13402 df-seq 14066 df-exp 14126 df-cj 15186 df-re 15187 df-im 15188 df-sqrt 15322 df-abs 15323 df-topgen 17528 df-psmet 21577 df-xmet 21578 df-met 21579 df-bl 21580 df-mopn 21581 df-bases 23171

This theorem is used by: qdensere2 25023 rehaus 25025 resubmet 25028 tgioo2 25029 xrsmopn 25039 iccntr 25048 icccmplem3 25051 reconnlem2 25054 opnreen 25058 metdscn2 25084 evthicc 25687 opnmbllem 25829 dvlip2 26222 lhop 26243 dvcnvre 26246 nmcvcn 31176 opnrebl 36939 opnrebl2 36940 ptrecube 38369 poimirlem30 38399 opnmbllem0 38405 reheibor 38589

W3C validator