opnmbllem

		Ref	Expression
	Hypothesis	dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
	Assertion	opnmbllem	$⊢ A \in topGen (ran (.)) \to A \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
2		fveq2	$⊢ z = w \to [.] (z) = [.] (w)$
3	2	sseq1d	$⊢ z = w \to ([.] (z) \subseteq A \leftrightarrow [.] (w) \subseteq A)$
4	3	elrab	$⊢ w \in \{z \in ran F \| [.] (z) \subseteq A\} \leftrightarrow (w \in ran F \land [.] (w) \subseteq A)$
5		simprr	$⊢ (A \in topGen (ran (.)) \land (w \in ran F \land [.] (w) \subseteq A)) \to [.] (w) \subseteq A$
6		fvex	$⊢ [.] (w) \in V$
7	6	elpw	$⊢ [.] (w) \in 𝒫 A \leftrightarrow [.] (w) \subseteq A$
8	5 7	sylibr	$⊢ (A \in topGen (ran (.)) \land (w \in ran F \land [.] (w) \subseteq A)) \to [.] (w) \in 𝒫 A$
9	4 8	sylan2b	$⊢ (A \in topGen (ran (.)) \land w \in \{z \in ran F \| [.] (z) \subseteq A\}) \to [.] (w) \in 𝒫 A$
10	9	ralrimiva	$⊢ A \in topGen (ran (.)) \to \forall w \in \{z \in ran F \| [.] (z) \subseteq A\} [.] (w) \in 𝒫 A$
11		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
12		ffun	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*} \to Fun [.]$
13	11 12	ax-mp	$⊢ Fun [.]$
14		ssrab2	$⊢ \{z \in ran F \| [.] (z) \subseteq A\} \subseteq ran F$
15	1	dyadf	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$
16		frn	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to ran F \subseteq \leq \cap ℝ^{2}$
17	15 16	ax-mp	$⊢ ran F \subseteq \leq \cap ℝ^{2}$
18		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
19		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
20	18 19	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
21	17 20	sstri	$⊢ ran F \subseteq ℝ^{} \times ℝ^{}$
22	14 21	sstri	$⊢ \{z \in ran F \| [.] (z) \subseteq A\} \subseteq ℝ^{} \times ℝ^{}$
23	11	fdmi	$⊢ dom [.] = ℝ^{} \times ℝ^{}$
24	22 23	sseqtrri	$⊢ \{z \in ran F \| [.] (z) \subseteq A\} \subseteq dom [.]$
25		funimass4	$⊢ (Fun [.] \land \{z \in ran F \| [.] (z) \subseteq A\} \subseteq dom [.]) \to ([.] [\{z \in ran F \| [.] (z) \subseteq A\}] \subseteq 𝒫 A \leftrightarrow \forall w \in \{z \in ran F \| [.] (z) \subseteq A\} [.] (w) \in 𝒫 A)$
26	13 24 25	mp2an	$⊢ [.] [\{z \in ran F \| [.] (z) \subseteq A\}] \subseteq 𝒫 A \leftrightarrow \forall w \in \{z \in ran F \| [.] (z) \subseteq A\} [.] (w) \in 𝒫 A$
27	10 26	sylibr	$⊢ A \in topGen (ran (.)) \to [.] [\{z \in ran F \| [.] (z) \subseteq A\}] \subseteq 𝒫 A$
28		sspwuni	$⊢ [.] [\{z \in ran F \| [.] (z) \subseteq A\}] \subseteq 𝒫 A \leftrightarrow ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}] \subseteq A$
29	27 28	sylib	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}] \subseteq A$
30		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
31	30	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
32		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
33	30 32	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
34	33	mopni2	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land A \in topGen (ran (.)) \land w \in A) \to \exists r \in ℝ^{+} w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq A$
35	31 34	mp3an1	$⊢ (A \in topGen (ran (.)) \land w \in A) \to \exists r \in ℝ^{+} w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq A$
36		elssuni	$⊢ A \in topGen (ran (.)) \to A \subseteq ⋃ topGen (ran (.))$
37		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
38	36 37	sseqtrrdi	$⊢ A \in topGen (ran (.)) \to A \subseteq ℝ$
39	38	sselda	$⊢ (A \in topGen (ran (.)) \land w \in A) \to w \in ℝ$
40		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
41	30	bl2ioo	$⊢ (w \in ℝ \land r \in ℝ) \to w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (w - r, w + r)$
42	39 40 41	syl2an	$⊢ ((A \in topGen (ran (.)) \land w \in A) \land r \in ℝ^{+}) \to w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (w - r, w + r)$
43	42	sseq1d	$⊢ ((A \in topGen (ran (.)) \land w \in A) \land r \in ℝ^{+}) \to (w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq A \leftrightarrow (w - r, w + r) \subseteq A)$
44		2re	$⊢ 2 \in ℝ$
45		1lt2	$⊢ 1 < 2$
46		expnlbnd	$⊢ (r \in ℝ^{+} \land 2 \in ℝ \land 1 < 2) \to \exists n \in ℕ \frac{1}{2^{n}} < r$
47	44 45 46	mp3an23	$⊢ r \in ℝ^{+} \to \exists n \in ℕ \frac{1}{2^{n}} < r$
48	47	ad2antrl	$⊢ ((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \to \exists n \in ℕ \frac{1}{2^{n}} < r$
49	39	ad2antrr	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w \in ℝ$
50		2nn	$⊢ 2 \in ℕ$
51		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
52	51	ad2antrl	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to n \in ℕ_{0}$
53		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
54	50 52 53	sylancr	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to 2^{n} \in ℕ$
55	54	nnred	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to 2^{n} \in ℝ$
56	49 55	remulcld	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w 2^{n} \in ℝ$
57		fllelt	$⊢ w 2^{n} \in ℝ \to (⌊w 2^{n}⌋ \leq w 2^{n} \land w 2^{n} < ⌊w 2^{n}⌋ + 1)$
58	56 57	syl	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to (⌊w 2^{n}⌋ \leq w 2^{n} \land w 2^{n} < ⌊w 2^{n}⌋ + 1)$
59	58	simpld	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to ⌊w 2^{n}⌋ \leq w 2^{n}$
60		reflcl	$⊢ w 2^{n} \in ℝ \to ⌊w 2^{n}⌋ \in ℝ$
61	56 60	syl	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to ⌊w 2^{n}⌋ \in ℝ$
62	54	nngt0d	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to 0 < 2^{n}$
63		ledivmul2	$⊢ (⌊w 2^{n}⌋ \in ℝ \land w \in ℝ \land (2^{n} \in ℝ \land 0 < 2^{n})) \to (\frac{⌊w 2^{n}⌋}{2^{n}} \leq w \leftrightarrow ⌊w 2^{n}⌋ \leq w 2^{n})$
64	61 49 55 62 63	syl112anc	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to (\frac{⌊w 2^{n}⌋}{2^{n}} \leq w \leftrightarrow ⌊w 2^{n}⌋ \leq w 2^{n})$
65	59 64	mpbird	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to \frac{⌊w 2^{n}⌋}{2^{n}} \leq w$
66		peano2re	$⊢ ⌊w 2^{n}⌋ \in ℝ \to ⌊w 2^{n}⌋ + 1 \in ℝ$
67	61 66	syl	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to ⌊w 2^{n}⌋ + 1 \in ℝ$
68	67 54	nndivred	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to \frac{⌊w 2^{n}⌋ + 1}{2^{n}} \in ℝ$
69	58	simprd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w 2^{n} < ⌊w 2^{n}⌋ + 1$
70		ltmuldiv	$⊢ (w \in ℝ \land ⌊w 2^{n}⌋ + 1 \in ℝ \land (2^{n} \in ℝ \land 0 < 2^{n})) \to (w 2^{n} < ⌊w 2^{n}⌋ + 1 \leftrightarrow w < \frac{⌊w 2^{n}⌋ + 1}{2^{n}})$
71	49 67 55 62 70	syl112anc	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to (w 2^{n} < ⌊w 2^{n}⌋ + 1 \leftrightarrow w < \frac{⌊w 2^{n}⌋ + 1}{2^{n}})$
72	69 71	mpbid	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w < \frac{⌊w 2^{n}⌋ + 1}{2^{n}}$
73	49 68 72	ltled	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w \leq \frac{⌊w 2^{n}⌋ + 1}{2^{n}}$
74	61 54	nndivred	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to \frac{⌊w 2^{n}⌋}{2^{n}} \in ℝ$
75		elicc2	$⊢ (\frac{⌊w 2^{n}⌋}{2^{n}} \in ℝ \land \frac{⌊w 2^{n}⌋ + 1}{2^{n}} \in ℝ) \to (w \in [\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}] \leftrightarrow (w \in ℝ \land \frac{⌊w 2^{n}⌋}{2^{n}} \leq w \land w \leq \frac{⌊w 2^{n}⌋ + 1}{2^{n}}))$
76	74 68 75	syl2anc	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to (w \in [\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}] \leftrightarrow (w \in ℝ \land \frac{⌊w 2^{n}⌋}{2^{n}} \leq w \land w \leq \frac{⌊w 2^{n}⌋ + 1}{2^{n}}))$
77	49 65 73 76	mpbir3and	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w \in [\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}]$
78	56	flcld	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to ⌊w 2^{n}⌋ \in ℤ$
79	1	dyadval	$⊢ (⌊w 2^{n}⌋ \in ℤ \land n \in ℕ_{0}) \to ⌊w 2^{n}⌋ F n = ⟨\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}⟩$
80	78 52 79	syl2anc	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to ⌊w 2^{n}⌋ F n = ⟨\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}⟩$
81	80	fveq2d	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to [.] (⌊w 2^{n}⌋ F n) = [.] (⟨\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}⟩)$
82		df-ov	$⊢ [\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}] = [.] (⟨\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}⟩)$
83	81 82	eqtr4di	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to [.] (⌊w 2^{n}⌋ F n) = [\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}]$
84	77 83	eleqtrrd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w \in [.] (⌊w 2^{n}⌋ F n)$
85		fveq2	$⊢ z = ⌊w 2^{n}⌋ F n \to [.] (z) = [.] (⌊w 2^{n}⌋ F n)$
86	85	sseq1d	$⊢ z = ⌊w 2^{n}⌋ F n \to ([.] (z) \subseteq A \leftrightarrow [.] (⌊w 2^{n}⌋ F n) \subseteq A)$
87		ffn	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to F Fn (ℤ \times ℕ_{0})$
88	15 87	ax-mp	$⊢ F Fn (ℤ \times ℕ_{0})$
89		fnovrn	$⊢ (F Fn (ℤ \times ℕ_{0}) \land ⌊w 2^{n}⌋ \in ℤ \land n \in ℕ_{0}) \to ⌊w 2^{n}⌋ F n \in ran F$
90	88 78 52 89	mp3an2i	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to ⌊w 2^{n}⌋ F n \in ran F$
91		simplrl	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to r \in ℝ^{+}$
92	91	rpred	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to r \in ℝ$
93	49 92	resubcld	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w - r \in ℝ$
94	93	rexrd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w - r \in ℝ^{*}$
95	49 92	readdcld	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w + r \in ℝ$
96	95	rexrd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w + r \in ℝ^{*}$
97	74 92	readdcld	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to (\frac{⌊w 2^{n}⌋}{2^{n}}) + r \in ℝ$
98	61	recnd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to ⌊w 2^{n}⌋ \in ℂ$
99		1cnd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to 1 \in ℂ$
100	55	recnd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to 2^{n} \in ℂ$
101	54	nnne0d	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to 2^{n} \neq 0$
102	98 99 100 101	divdird	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to \frac{⌊w 2^{n}⌋ + 1}{2^{n}} = (\frac{⌊w 2^{n}⌋}{2^{n}}) + (\frac{1}{2^{n}})$
103	54	nnrecred	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to \frac{1}{2^{n}} \in ℝ$
104		simprr	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to \frac{1}{2^{n}} < r$
105	103 92 74 104	ltadd2dd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to (\frac{⌊w 2^{n}⌋}{2^{n}}) + (\frac{1}{2^{n}}) < (\frac{⌊w 2^{n}⌋}{2^{n}}) + r$
106	102 105	eqbrtrd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to \frac{⌊w 2^{n}⌋ + 1}{2^{n}} < (\frac{⌊w 2^{n}⌋}{2^{n}}) + r$
107	49 68 97 72 106	lttrd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w < (\frac{⌊w 2^{n}⌋}{2^{n}}) + r$
108	49 92 74	ltsubaddd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to (w - r < \frac{⌊w 2^{n}⌋}{2^{n}} \leftrightarrow w < (\frac{⌊w 2^{n}⌋}{2^{n}}) + r)$
109	107 108	mpbird	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w - r < \frac{⌊w 2^{n}⌋}{2^{n}}$
110	49 103	readdcld	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w + (\frac{1}{2^{n}}) \in ℝ$
111	74 49 103 65	leadd1dd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to (\frac{⌊w 2^{n}⌋}{2^{n}}) + (\frac{1}{2^{n}}) \leq w + (\frac{1}{2^{n}})$
112	102 111	eqbrtrd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to \frac{⌊w 2^{n}⌋ + 1}{2^{n}} \leq w + (\frac{1}{2^{n}})$
113	103 92 49 104	ltadd2dd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w + (\frac{1}{2^{n}}) < w + r$
114	68 110 95 112 113	lelttrd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to \frac{⌊w 2^{n}⌋ + 1}{2^{n}} < w + r$
115		iccssioo	$⊢ ((w - r \in ℝ^{} \land w + r \in ℝ^{}) \land (w - r < \frac{⌊w 2^{n}⌋}{2^{n}} \land \frac{⌊w 2^{n}⌋ + 1}{2^{n}} < w + r)) \to [\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}] \subseteq (w - r, w + r)$
116	94 96 109 114 115	syl22anc	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to [\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}] \subseteq (w - r, w + r)$
117	83 116	eqsstrd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to [.] (⌊w 2^{n}⌋ F n) \subseteq (w - r, w + r)$
118		simplrr	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to (w - r, w + r) \subseteq A$
119	117 118	sstrd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to [.] (⌊w 2^{n}⌋ F n) \subseteq A$
120	86 90 119	elrabd	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to ⌊w 2^{n}⌋ F n \in \{z \in ran F \| [.] (z) \subseteq A\}$
121		funfvima2	$⊢ (Fun [.] \land \{z \in ran F \| [.] (z) \subseteq A\} \subseteq dom [.]) \to (⌊w 2^{n}⌋ F n \in \{z \in ran F \| [.] (z) \subseteq A\} \to [.] (⌊w 2^{n}⌋ F n) \in [.] [\{z \in ran F \| [.] (z) \subseteq A\}])$
122	13 24 121	mp2an	$⊢ ⌊w 2^{n}⌋ F n \in \{z \in ran F \| [.] (z) \subseteq A\} \to [.] (⌊w 2^{n}⌋ F n) \in [.] [\{z \in ran F \| [.] (z) \subseteq A\}]$
123	120 122	syl	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to [.] (⌊w 2^{n}⌋ F n) \in [.] [\{z \in ran F \| [.] (z) \subseteq A\}]$
124		elunii	$⊢ (w \in [.] (⌊w 2^{n}⌋ F n) \land [.] (⌊w 2^{n}⌋ F n) \in [.] [\{z \in ran F \| [.] (z) \subseteq A\}]) \to w \in ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}]$
125	84 123 124	syl2anc	$⊢ (((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \land (n \in ℕ \land \frac{1}{2^{n}} < r)) \to w \in ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}]$
126	48 125	rexlimddv	$⊢ ((A \in topGen (ran (.)) \land w \in A) \land (r \in ℝ^{+} \land (w - r, w + r) \subseteq A)) \to w \in ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}]$
127	126	expr	$⊢ ((A \in topGen (ran (.)) \land w \in A) \land r \in ℝ^{+}) \to ((w - r, w + r) \subseteq A \to w \in ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}])$
128	43 127	sylbid	$⊢ ((A \in topGen (ran (.)) \land w \in A) \land r \in ℝ^{+}) \to (w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq A \to w \in ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}])$
129	128	rexlimdva	$⊢ (A \in topGen (ran (.)) \land w \in A) \to (\exists r \in ℝ^{+} w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq A \to w \in ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}])$
130	35 129	mpd	$⊢ (A \in topGen (ran (.)) \land w \in A) \to w \in ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}]$
131	29 130	eqelssd	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}] = A$
132		fveq2	$⊢ c = a \to [.] (c) = [.] (a)$
133	132	sseq1d	$⊢ c = a \to ([.] (c) \subseteq [.] (b) \leftrightarrow [.] (a) \subseteq [.] (b))$
134		equequ1	$⊢ c = a \to (c = b \leftrightarrow a = b)$
135	133 134	imbi12d	$⊢ c = a \to (([.] (c) \subseteq [.] (b) \to c = b) \leftrightarrow ([.] (a) \subseteq [.] (b) \to a = b))$
136	135	ralbidv	$⊢ c = a \to (\forall b \in \{z \in ran F \| [.] (z) \subseteq A\} ([.] (c) \subseteq [.] (b) \to c = b) \leftrightarrow \forall b \in \{z \in ran F \| [.] (z) \subseteq A\} ([.] (a) \subseteq [.] (b) \to a = b))$
137	136	cbvrabv	$⊢ \{c \in \{z \in ran F \| [.] (z) \subseteq A\} \| \forall b \in \{z \in ran F \| [.] (z) \subseteq A\} ([.] (c) \subseteq [.] (b) \to c = b)\} = \{a \in \{z \in ran F \| [.] (z) \subseteq A\} \| \forall b \in \{z \in ran F \| [.] (z) \subseteq A\} ([.] (a) \subseteq [.] (b) \to a = b)\}$
138	14	a1i	$⊢ A \in topGen (ran (.)) \to \{z \in ran F \| [.] (z) \subseteq A\} \subseteq ran F$
139	1 137 138	dyadmbl	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{z \in ran F \| [.] (z) \subseteq A\}] \in dom vol$
140	131 139	eqeltrrd	$⊢ A \in topGen (ran (.)) \to A \in dom vol$

Metamath Proof Explorer

Theorem opnmbllem

Proof