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 25159

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 25154	. . 3 ⊢ 𝐷 ∈ (∞Met‘ℝ)
3		tgioo.2	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐷)
4	3	mopnval 24801	. . 3 ⊢ (𝐷 ∈ (∞Met‘ℝ) → 𝐽 = (topGen‘ran (ball‘𝐷)))
5	2, 4	ax-mp 5	. 2 ⊢ 𝐽 = (topGen‘ran (ball‘𝐷))
6	1	blssioo 25158	. . 3 ⊢ ran (ball‘𝐷) ⊆ ran (,)
7		elssuni 4902	. . . . . . 7 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,))
8		unirnioo 13618	. . . . . . 7 ⊢ ℝ = ∪ ran (,)
9	7, 8	sseqtrrdi 3954	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → 𝑣 ⊆ ℝ)
10		retopbas 25123	. . . . . . . . . 10 ⊢ ran (,) ∈ TopBases
11	10	a1i 11	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ran (,) ∈ TopBases)
12		simpl 488	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ran (,))
13	9	sselda 3913	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ℝ)
14		1re 11345	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
15	1	bl2ioo 25155	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
16	14, 15	mpan2 704	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
17		ioof 13616	. . . . . . . . . . . . 13 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
18		ffn 6737	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
19	17, 18	ax-mp 5	. . . . . . . . . . . 12 ⊢ (,) Fn (ℝ^* × ℝ^*)
20		peano2rem 11662	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ)
21	20	rexrd 11396	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈ ℝ^*)
22		peano2re 11520	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
23	22	rexrd 11396	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ^*)
24		fnovrn 7626	. . . . . . . . . . . 12 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ (𝑥 − 1) ∈ ℝ^ ∧ (𝑥 + 1) ∈ ℝ^*) → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
25	19, 21, 23, 24	mp3an2i 1496	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1)(,)(𝑥 + 1)) ∈ ran (,))
26	16, 25	eqeltrd 2864	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑥(ball‘𝐷)1) ∈ ran (,))
27	13, 26	syl 18	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝐷)1) ∈ ran (,))
28		simpr 490	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣)
29		1rp 13162	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
30		blcntr 24776	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘ℝ) ∧ 𝑥 ∈ ℝ ∧ 1 ∈ ℝ⁺) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
31	2, 29, 30	mp3an13 1482	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥(ball‘𝐷)1))
32	13, 31	syl 18	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑥(ball‘𝐷)1))
33	28, 32	elind 4100	. . . . . . . . 9 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑣 ∩ (𝑥(ball‘𝐷)1)))
34		basis2 23313	. . . . . . . . 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 7627	. . . . . . . . . . 11 ⊢ ((,) Fn (ℝ^* × ℝ^) → (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ^ ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏)))
37	19, 36	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑧 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ^* ∃𝑏 ∈ ℝ^* 𝑧 = (𝑎(,)𝑏))
38		eleq2 2853	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑎(,)𝑏)))
39		sseq1 3938	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ↔ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))))
40	38, 39	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)))))
41		inss2 4137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ (𝑥(ball‘𝐷)1)
42		sstr 3921	. . . . . . . . . . . . . . . . . . . . . 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 13544	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
46	45	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ ℝ)
47	46, 16	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥(ball‘𝐷)1) = ((𝑥 − 1)(,)(𝑥 + 1)))
48	44, 47	sseqtrd 3949	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)))
49		dfss 4098	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎(,)𝑏) ⊆ ((𝑥 − 1)(,)(𝑥 + 1)) ↔ (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
50	48, 49	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = ((𝑎(,)𝑏) ∩ ((𝑥 − 1)(,)(𝑥 + 1))))
51		eliooxr 13573	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^*))
52	21, 23	jca 521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 1) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*))
53	45, 52	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑥 − 1) ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*))
54		iooin 13548	. . . . . . . . . . . . . . . . . . . 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 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) = (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
58		mnfxr 11403	. . . . . . . . . . . . . . . . . . . 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 4532	. . . . . . . . . . . . . . . . . . 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 11396	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 + 1) ∈ ℝ^*)
67	64, 66	ifcld 4532	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*)
68	45, 20	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝑎(,)𝑏) → (𝑥 − 1) ∈ ℝ)
69	68	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑥 − 1) ∈ ℝ)
70	69	mnfltd 13291	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < (𝑥 − 1))
71		xrmax2 13344	. . . . . . . . . . . . . . . . . . . . 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 13328	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎))
74		simpl 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (𝑎(,)𝑏))
75	74, 57	eleqtrd 2866	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → 𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))))
76		eliooxr 13573	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ^* ∧ if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ∈ ℝ^*))
77		ne0i 4290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) → (if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎)(,)if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1))) ≠ ∅)
78		ioon0 13540	. . . . . . . . . . . . . . . . . . . . . 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 13338	. . . . . . . . . . . . . . . . . . 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 1406	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑎 ≤ (𝑥 − 1), (𝑥 − 1), 𝑎) ∈ ℝ)
84		mnfle 13302	. . . . . . . . . . . . . . . . . . . . 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 13327	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → -∞ < if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)))
87		xrmin2 13346	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ ℝ^* ∧ (𝑥 + 1) ∈ ℝ^*) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))
88	64, 66, 87	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → if(𝑏 ≤ (𝑥 + 1), 𝑏, (𝑥 + 1)) ≤ (𝑥 + 1))
89		xrre 13337	. . . . . . . . . . . . . . . . . . 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 25157	. . . . . . . . . . . . . . . . . 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 2864	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ∈ ran (ball‘𝐷))
94		inss1 4136	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣
95		sstr 3921	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ∧ (𝑣 ∩ (𝑥(ball‘𝐷)1)) ⊆ 𝑣) → (𝑎(,)𝑏) ⊆ 𝑣)
96	94, 95	mpan2 704	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1)) → (𝑎(,)𝑏) ⊆ 𝑣)
97	96	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → (𝑎(,)𝑏) ⊆ 𝑣)
98		sseq1 3938	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑎(,)𝑏) → (𝑧 ⊆ 𝑣 ↔ (𝑎(,)𝑏) ⊆ 𝑣))
99	38, 98	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎(,)𝑏) → ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣) ↔ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)))
100	99	rspcev 3580	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎(,)𝑏) ∈ ran (ball‘𝐷) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
101	93, 74, 97, 100	syl12anc 850	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑧 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣))
102		blssex 24790	. . . . . . . . . . . . . . . 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 3208	. . . . . . . . . . 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 3159	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran (,)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ (𝑣 ∩ (𝑥(ball‘𝐷)1))) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
111	35, 110	syl 18	. . . . . . 7 ⊢ ((𝑣 ∈ ran (,) ∧ 𝑥 ∈ 𝑣) → ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
112	111	ralrimiva 3158	. . . . . 6 ⊢ (𝑣 ∈ ran (,) → ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)
113	3	elmopn2 24808	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘ℝ) → (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣)))
114	2, 113	ax-mp 5	. . . . . 6 ⊢ (𝑣 ∈ 𝐽 ↔ (𝑣 ⊆ ℝ ∧ ∀𝑥 ∈ 𝑣 ∃𝑦 ∈ ℝ⁺ (𝑥(ball‘𝐷)𝑦) ⊆ 𝑣))
115	9, 112, 114	sylanbrc 595	. . . . 5 ⊢ (𝑣 ∈ ran (,) → 𝑣 ∈ 𝐽)
116	115	ssriv 3917	. . . 4 ⊢ ran (,) ⊆ 𝐽
117	116, 5	sseqtri 3961	. . 3 ⊢ ran (,) ⊆ (topGen‘ran (ball‘𝐷))
118		2basgen 23352	. . 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 2787	1 ⊢ (topGen‘ran (,)) = 𝐽

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 ⊆ wss 3900 ∩ cin 4092 ∅c0 4281 ifcif 4485 𝒫 cpw 4560 ∪ cuni 4870 class class class wbr 5106 × cxp 5654 ran crn 5657 ↾ cres 5658 ∘ ccom 5660 Fn wfn 6559 ⟶wf 6560 ‘cfv 6564 (class class class)co 7449 ℝcr 11236 1c1 11238 + caddc 11240 -∞cmnf 11378 ℝ^*cxr 11379 < clt 11380 ≤ cle 11381 − cmin 11578 ℝ⁺crp 13158 (,)cioo 13514 abscabs 15442 topGenctg 17649 ∞Metcxmet 21705 ballcbl 21707 MetOpencmopn 21710 TopBasesctb 23307

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314 ax-pre-sup 11315

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-om 7910 df-1st 8033 df-2nd 8034 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-er 8753 df-map 8885 df-en 9010 df-dom 9011 df-sdom 9012 df-sup 9469 df-inf 9470 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-div 12012 df-nn 12374 df-2 12443 df-3 12444 df-n0 12645 df-z 12732 df-uz 13004 df-q 13114 df-rp 13159 df-xneg 13279 df-xadd 13280 df-xmul 13281 df-ioo 13518 df-seq 14183 df-exp 14243 df-cj 15307 df-re 15308 df-im 15309 df-sqrt 15443 df-abs 15444 df-topgen 17655 df-psmet 21712 df-xmet 21713 df-met 21714 df-bl 21715 df-mopn 21716 df-bases 23308

This theorem is used by: qdensere2 25160 rehaus 25162 resubmet 25165 tgioo2 25166 xrsmopn 25176 iccntr 25185 icccmplem3 25188 reconnlem2 25191 opnreen 25195 metdscn2 25221 evthicc 25824 opnmbllem 25966 dvlip2 26359 lhop 26380 dvcnvre 26383 nmcvcn 31343 opnrebl 37316 opnrebl2 37317 ptrecube 38799 poimirlem30 38829 opnmbllem0 38835 reheibor 39032

W3C validator