opnmbllem - Metamath Proof Explorer

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

Theorem opnmbllem 25440

Description: Lemma for opnmbl 25441. (Contributed by Mario Carneiro, 26-Mar-2015.)

**Hypothesis**
Ref	Expression
dyadmbl.1	⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)

**Assertion**
Ref	Expression
opnmbllem	⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐹,𝑦

Proof of Theorem opnmbllem Dummy variables 𝑐 𝑎 𝑏 𝑛 𝑤 𝑧 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6881	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → ([,]‘𝑧) = ([,]‘𝑤))
2	1	sseq1d 4005	. . . . . . . 8 ⊢ (𝑧 = 𝑤 → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘𝑤) ⊆ 𝐴))
3	2	elrab 3675	. . . . . . 7 ⊢ (𝑤 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ↔ (𝑤 ∈ ran 𝐹 ∧ ([,]‘𝑤) ⊆ 𝐴))
4		simprr 770	. . . . . . . 8 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ (𝑤 ∈ ran 𝐹 ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ⊆ 𝐴)
5		fvex 6894	. . . . . . . . 9 ⊢ ([,]‘𝑤) ∈ V
6	5	elpw 4598	. . . . . . . 8 ⊢ (([,]‘𝑤) ∈ 𝒫 𝐴 ↔ ([,]‘𝑤) ⊆ 𝐴)
7	4, 6	sylibr 233	. . . . . . 7 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ (𝑤 ∈ ran 𝐹 ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ∈ 𝒫 𝐴)
8	3, 7	sylan2b 593	. . . . . 6 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) → ([,]‘𝑤) ∈ 𝒫 𝐴)
9	8	ralrimiva 3138	. . . . 5 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∀𝑤 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴)
10		iccf 13421	. . . . . . 7 ⊢ [,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^
11		ffun 6710	. . . . . . 7 ⊢ ([,]:(ℝ^* × ℝ^)⟶𝒫 ℝ^ → Fun [,])
12	10, 11	ax-mp 5	. . . . . 6 ⊢ Fun [,]
13		ssrab2 4069	. . . . . . . 8 ⊢ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ ran 𝐹
14		dyadmbl.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ₀ ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)
15	14	dyadf 25430	. . . . . . . . . 10 ⊢ 𝐹:(ℤ × ℕ₀)⟶( ≤ ∩ (ℝ × ℝ))
16		frn 6714	. . . . . . . . . 10 ⊢ (𝐹:(ℤ × ℕ₀)⟶( ≤ ∩ (ℝ × ℝ)) → ran 𝐹 ⊆ ( ≤ ∩ (ℝ × ℝ)))
17	15, 16	ax-mp 5	. . . . . . . . 9 ⊢ ran 𝐹 ⊆ ( ≤ ∩ (ℝ × ℝ))
18		inss2 4221	. . . . . . . . . 10 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
19		rexpssxrxp 11255	. . . . . . . . . 10 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
20	18, 19	sstri 3983	. . . . . . . . 9 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
21	17, 20	sstri 3983	. . . . . . . 8 ⊢ ran 𝐹 ⊆ (ℝ^* × ℝ^*)
22	13, 21	sstri 3983	. . . . . . 7 ⊢ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ (ℝ^* × ℝ^*)
23	10	fdmi 6719	. . . . . . 7 ⊢ dom [,] = (ℝ^* × ℝ^*)
24	22, 23	sseqtrri 4011	. . . . . 6 ⊢ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]
25		funimass4 6946	. . . . . 6 ⊢ ((Fun [,] ∧ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) → (([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴))
26	12, 24, 25	mp2an 689	. . . . 5 ⊢ (([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴)
27	9, 26	sylibr 233	. . . 4 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴)
28		sspwuni 5093	. . . 4 ⊢ (([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴)
29	27, 28	sylib 217	. . 3 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴)
30		eqid 2724	. . . . . 6 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
31	30	rexmet 24617	. . . . 5 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
32		eqid 2724	. . . . . . 7 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
33	30, 32	tgioo 24622	. . . . . 6 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
34	33	mopni2 24312	. . . . 5 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → ∃𝑟 ∈ ℝ⁺ (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴)
35	31, 34	mp3an1 1444	. . . 4 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → ∃𝑟 ∈ ℝ⁺ (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴)
36		elssuni 4931	. . . . . . . . . 10 ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ⊆ ∪ (topGen‘ran (,)))
37		uniretop 24589	. . . . . . . . . 10 ⊢ ℝ = ∪ (topGen‘ran (,))
38	36, 37	sseqtrrdi 4025	. . . . . . . . 9 ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ⊆ ℝ)
39	38	sselda 3974	. . . . . . . 8 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ)
40		rpre 12978	. . . . . . . 8 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
41	30	bl2ioo 24618	. . . . . . . 8 ⊢ ((𝑤 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
42	39, 40, 41	syl2an 595	. . . . . . 7 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ⁺) → (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
43	42	sseq1d 4005	. . . . . 6 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ⁺) → ((𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 ↔ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴))
44		2re 12282	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
45		1lt2 12379	. . . . . . . . . 10 ⊢ 1 < 2
46		expnlbnd 14192	. . . . . . . . . 10 ⊢ ((𝑟 ∈ ℝ⁺ ∧ 2 ∈ ℝ ∧ 1 < 2) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟)
47	44, 45, 46	mp3an23 1449	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ⁺ → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟)
48	47	ad2antrl 725	. . . . . . . 8 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟)
49	39	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ℝ)
50		2nn 12281	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ
51		nnnn0 12475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
52	51	ad2antrl 725	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑛 ∈ ℕ₀)
53		nnexpcl 14036	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℕ)
54	50, 52, 53	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℕ)
55	54	nnred 12223	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℝ)
56	49, 55	remulcld 11240	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) ∈ ℝ)
57		fllelt 13758	. . . . . . . . . . . . . 14 ⊢ ((𝑤 · (2↑𝑛)) ∈ ℝ → ((⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1)))
58	56, 57	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1)))
59	58	simpld 494	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)))
60		reflcl 13757	. . . . . . . . . . . . . 14 ⊢ ((𝑤 · (2↑𝑛)) ∈ ℝ → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ)
61	56, 60	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ)
62	54	nngt0d 12257	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 0 < (2↑𝑛))
63		ledivmul2 12089	. . . . . . . . . . . . 13 ⊢ (((⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛))))
64	61, 49, 55, 62, 63	syl112anc 1371	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛))))
65	59, 64	mpbird 257	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤)
66		peano2re 11383	. . . . . . . . . . . . . 14 ⊢ ((⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ)
67	61, 66	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ)
68	67, 54	nndivred 12262	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ∈ ℝ)
69	58	simprd 495	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1))
70		ltmuldiv 12083	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
71	49, 67, 55, 62, 70	syl112anc 1371	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
72	69, 71	mpbid 231	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))
73	49, 68, 72	ltled 11358	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))
74	61, 54	nndivred 12262	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∈ ℝ)
75		elicc2 13385	. . . . . . . . . . . 12 ⊢ ((((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∈ ℝ ∧ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ∈ ℝ) → (𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ∧ 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))))
76	74, 68, 75	syl2anc 583	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ∧ 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))))
77	49, 65, 73, 76	mpbir3and 1339	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
78	56	flcld 13759	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ)
79	14	dyadval 25431	. . . . . . . . . . . . 13 ⊢ (((⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) = ⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩)
80	78, 52, 79	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) = ⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩)
81	80	fveq2d 6885	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) = ([,]‘⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩))
82		df-ov 7404	. . . . . . . . . . 11 ⊢ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) = ([,]‘⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩)
83	81, 82	eqtr4di 2782	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
84	77, 83	eleqtrrd 2828	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)))
85		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) → ([,]‘𝑧) = ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)))
86	85	sseq1d 4005	. . . . . . . . . . 11 ⊢ (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ⊆ 𝐴))
87		ffn 6707	. . . . . . . . . . . . 13 ⊢ (𝐹:(ℤ × ℕ₀)⟶( ≤ ∩ (ℝ × ℝ)) → 𝐹 Fn (ℤ × ℕ₀))
88	15, 87	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝐹 Fn (ℤ × ℕ₀)
89		fnovrn 7575	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn (ℤ × ℕ₀) ∧ (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) ∈ ran 𝐹)
90	88, 78, 52, 89	mp3an2i 1462	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) ∈ ran 𝐹)
91		simplrl 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ⁺)
92	91	rpred 13012	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ)
93	49, 92	resubcld 11638	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) ∈ ℝ)
94	93	rexrd 11260	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) ∈ ℝ^*)
95	49, 92	readdcld 11239	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈ ℝ)
96	95	rexrd 11260	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈ ℝ^*)
97	74, 92	readdcld 11239	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟) ∈ ℝ)
98	61	recnd 11238	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℂ)
99		1cnd 11205	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 1 ∈ ℂ)
100	55	recnd 11238	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℂ)
101	54	nnne0d 12258	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ≠ 0)
102	98, 99, 100, 101	divdird 12024	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))))
103	54	nnrecred 12259	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) ∈ ℝ)
104		simprr 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) < 𝑟)
105	103, 92, 74, 104	ltadd2dd 11369	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))
106	102, 105	eqbrtrd 5160	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))
107	49, 68, 97, 72, 106	lttrd 11371	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))
108	49, 92, 74	ltsubaddd 11806	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟)))
109	107, 108	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)))
110	49, 103	readdcld 11239	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) ∈ ℝ)
111	74, 49, 103, 65	leadd1dd 11824	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) ≤ (𝑤 + (1 / (2↑𝑛))))
112	102, 111	eqbrtrd 5160	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ≤ (𝑤 + (1 / (2↑𝑛))))
113	103, 92, 49, 104	ltadd2dd 11369	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) < (𝑤 + 𝑟))
114	68, 110, 95, 112, 113	lelttrd 11368	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟))
115		iccssioo 13389	. . . . . . . . . . . . . 14 ⊢ ((((𝑤 − 𝑟) ∈ ℝ^* ∧ (𝑤 + 𝑟) ∈ ℝ^*) ∧ ((𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∧ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟))) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
116	94, 96, 109, 114, 115	syl22anc 836	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
117	83, 116	eqsstrd 4012	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)))
118		simplrr 775	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)
119	117, 118	sstrd 3984	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ⊆ 𝐴)
120	86, 90, 119	elrabd 3677	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})
121		funfvima2 7224	. . . . . . . . . . 11 ⊢ ((Fun [,] ∧ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) → (((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∈ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})))
122	12, 24, 121	mp2an 689	. . . . . . . . . 10 ⊢ (((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∈ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))
123	120, 122	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∈ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))
124		elunii 4904	. . . . . . . . 9 ⊢ ((𝑤 ∈ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∧ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∈ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})) → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))
125	84, 123, 124	syl2anc 583	. . . . . . . 8 ⊢ ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))
126	48, 125	rexlimddv 3153	. . . . . . 7 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ⁺ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))
127	126	expr 456	. . . . . 6 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ⁺) → (((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})))
128	43, 127	sylbid 239	. . . . 5 ⊢ (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ⁺) → ((𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})))
129	128	rexlimdva 3147	. . . 4 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → (∃𝑟 ∈ ℝ⁺ (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})))
130	35, 129	mpd 15	. . 3 ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))
131	29, 130	eqelssd 3995	. 2 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴)
132		fveq2 6881	. . . . . . 7 ⊢ (𝑐 = 𝑎 → ([,]‘𝑐) = ([,]‘𝑎))
133	132	sseq1d 4005	. . . . . 6 ⊢ (𝑐 = 𝑎 → (([,]‘𝑐) ⊆ ([,]‘𝑏) ↔ ([,]‘𝑎) ⊆ ([,]‘𝑏)))
134		equequ1 2020	. . . . . 6 ⊢ (𝑐 = 𝑎 → (𝑐 = 𝑏 ↔ 𝑎 = 𝑏))
135	133, 134	imbi12d 344	. . . . 5 ⊢ (𝑐 = 𝑎 → ((([,]‘𝑐) ⊆ ([,]‘𝑏) → 𝑐 = 𝑏) ↔ (([,]‘𝑎) ⊆ ([,]‘𝑏) → 𝑎 = 𝑏)))
136	135	ralbidv 3169	. . . 4 ⊢ (𝑐 = 𝑎 → (∀𝑏 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} (([,]‘𝑐) ⊆ ([,]‘𝑏) → 𝑐 = 𝑏) ↔ ∀𝑏 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑏) → 𝑎 = 𝑏)))
137	136	cbvrabv 3434	. . 3 ⊢ {𝑐 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ∣ ∀𝑏 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} (([,]‘𝑐) ⊆ ([,]‘𝑏) → 𝑐 = 𝑏)} = {𝑎 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ∣ ∀𝑏 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑏) → 𝑎 = 𝑏)}
138	13	a1i 11	. . 3 ⊢ (𝐴 ∈ (topGen‘ran (,)) → {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ ran 𝐹)
139	14, 137, 138	dyadmbl 25439	. 2 ⊢ (𝐴 ∈ (topGen‘ran (,)) → ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ∈ dom vol)
140	131, 139	eqeltrrd 2826	1 ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∀wral 3053 ∃wrex 3062 {crab 3424 ∩ cin 3939 ⊆ wss 3940 𝒫 cpw 4594 ⟨cop 4626 ∪ cuni 4899 class class class wbr 5138 × cxp 5664 dom cdm 5666 ran crn 5667 ↾ cres 5668 “ cima 5669 ∘ ccom 5670 Fun wfun 6527 Fn wfn 6528 ⟶wf 6529 ‘cfv 6533 (class class class)co 7401 ∈ cmpo 7403 ℝcr 11104 0cc0 11105 1c1 11106 + caddc 11108 · cmul 11110 ℝ^*cxr 11243 < clt 11244 ≤ cle 11245 − cmin 11440 / cdiv 11867 ℕcn 12208 2c2 12263 ℕ₀cn0 12468 ℤcz 12554 ℝ⁺crp 12970 (,)cioo 13320 [,]cicc 13323 ⌊cfl 13751 ↑cexp 14023 abscabs 15177 topGenctg 17379 ∞Metcxmet 21208 ballcbl 21210 MetOpencmopn 21213 volcvol 25302

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-inf2 9631 ax-cnex 11161 ax-resscn 11162 ax-1cn 11163 ax-icn 11164 ax-addcl 11165 ax-addrcl 11166 ax-mulcl 11167 ax-mulrcl 11168 ax-mulcom 11169 ax-addass 11170 ax-mulass 11171 ax-distr 11172 ax-i2m1 11173 ax-1ne0 11174 ax-1rid 11175 ax-rnegex 11176 ax-rrecex 11177 ax-cnre 11178 ax-pre-lttri 11179 ax-pre-lttrn 11180 ax-pre-ltadd 11181 ax-pre-mulgt0 11182 ax-pre-sup 11183

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-int 4941 df-iun 4989 df-disj 5104 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-se 5622 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-of 7663 df-om 7849 df-1st 7968 df-2nd 7969 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-2o 8462 df-oadd 8465 df-omul 8466 df-er 8698 df-map 8817 df-pm 8818 df-en 8935 df-dom 8936 df-sdom 8937 df-fin 8938 df-fi 9401 df-sup 9432 df-inf 9433 df-oi 9500 df-dju 9891 df-card 9929 df-acn 9932 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-n0 12469 df-z 12555 df-uz 12819 df-q 12929 df-rp 12971 df-xneg 13088 df-xadd 13089 df-xmul 13090 df-ioo 13324 df-ico 13326 df-icc 13327 df-fz 13481 df-fzo 13624 df-fl 13753 df-seq 13963 df-exp 14024 df-hash 14287 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-clim 15428 df-rlim 15429 df-sum 15629 df-rest 17364 df-topgen 17385 df-psmet 21215 df-xmet 21216 df-met 21217 df-bl 21218 df-mopn 21219 df-top 22706 df-topon 22723 df-bases 22759 df-cmp 23201 df-ovol 25303 df-vol 25304

This theorem is referenced by: opnmbl 25441

W3C validator