opnmbllem0

Description: Lemma for ismblfin ; could also be used to shorten proof of opnmbllem . (Contributed by Brendan Leahy, 13-Jul-2018)

		Ref	Expression
	Assertion	opnmbllem0	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}] = A$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ z = w \to [.] (z) = [.] (w)$
2	1	sseq1d	$⊢ z = w \to ([.] (z) \subseteq A \leftrightarrow [.] (w) \subseteq A)$
3	2	elrab	$⊢ w \in \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} \leftrightarrow (w \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \land [.] (w) \subseteq A)$
4		simprr	$⊢ (A \in topGen (ran (.)) \land (w \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \land [.] (w) \subseteq A)) \to [.] (w) \subseteq A$
5		fvex	$⊢ [.] (w) \in V$
6	5	elpw	$⊢ [.] (w) \in 𝒫 A \leftrightarrow [.] (w) \subseteq A$
7	4 6	sylibr	$⊢ (A \in topGen (ran (.)) \land (w \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \land [.] (w) \subseteq A)) \to [.] (w) \in 𝒫 A$
8	3 7	sylan2b	$⊢ (A \in topGen (ran (.)) \land w \in \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}) \to [.] (w) \in 𝒫 A$
9	8	ralrimiva	$⊢ A \in topGen (ran (.)) \to \forall w \in \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} [.] (w) \in 𝒫 A$
10		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
11		ffun	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*} \to Fun [.]$
12	10 11	ax-mp	$⊢ Fun [.]$
13		ssrab2	$⊢ \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} \subseteq ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
14		oveq1	$⊢ x = r \to \frac{x}{2^{y}} = \frac{r}{2^{y}}$
15		oveq1	$⊢ x = r \to x + 1 = r + 1$
16	15	oveq1d	$⊢ x = r \to \frac{x + 1}{2^{y}} = \frac{r + 1}{2^{y}}$
17	14 16	opeq12d	$⊢ x = r \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ = ⟨\frac{r}{2^{y}}, \frac{r + 1}{2^{y}}⟩$
18		oveq2	$⊢ y = s \to 2^{y} = 2^{s}$
19	18	oveq2d	$⊢ y = s \to \frac{r}{2^{y}} = \frac{r}{2^{s}}$
20	18	oveq2d	$⊢ y = s \to \frac{r + 1}{2^{y}} = \frac{r + 1}{2^{s}}$
21	19 20	opeq12d	$⊢ y = s \to ⟨\frac{r}{2^{y}}, \frac{r + 1}{2^{y}}⟩ = ⟨\frac{r}{2^{s}}, \frac{r + 1}{2^{s}}⟩$
22	17 21	cbvmpov	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) = (r \in ℤ, s \in ℕ_{0} ⟼ ⟨\frac{r}{2^{s}}, \frac{r + 1}{2^{s}}⟩)$
23	22	dyadf	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$
24		frn	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq \leq \cap ℝ^{2}$
25	23 24	ax-mp	$⊢ ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq \leq \cap ℝ^{2}$
26		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
27		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
28	26 27	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
29	25 28	sstri	$⊢ ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq ℝ^{} \times ℝ^{}$
30	13 29	sstri	$⊢ \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} \subseteq ℝ^{} \times ℝ^{}$
31	10	fdmi	$⊢ dom [.] = ℝ^{} \times ℝ^{}$
32	30 31	sseqtrri	$⊢ \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} \subseteq dom [.]$
33		funimass4	$⊢ (Fun [.] \land \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} \subseteq dom [.]) \to ([.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}] \subseteq 𝒫 A \leftrightarrow \forall w \in \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} [.] (w) \in 𝒫 A)$
34	12 32 33	mp2an	$⊢ [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}] \subseteq 𝒫 A \leftrightarrow \forall w \in \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} [.] (w) \in 𝒫 A$
35	9 34	sylibr	$⊢ A \in topGen (ran (.)) \to [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}] \subseteq 𝒫 A$
36		sspwuni	$⊢ [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}] \subseteq 𝒫 A \leftrightarrow ⋃ [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}] \subseteq A$
37	35 36	sylib	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}] \subseteq A$
38		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
39	38	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
40		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
41	38 40	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
42	41	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$
43	39 42	mp3an1	$⊢ (A \in topGen (ran (.)) \land w \in A) \to \exists r \in ℝ^{+} w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq A$
44		elssuni	$⊢ A \in topGen (ran (.)) \to A \subseteq ⋃ topGen (ran (.))$
45		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
46	44 45	sseqtrrdi	$⊢ A \in topGen (ran (.)) \to A \subseteq ℝ$
47	46	sselda	$⊢ (A \in topGen (ran (.)) \land w \in A) \to w \in ℝ$
48		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
49	38	bl2ioo	$⊢ (w \in ℝ \land r \in ℝ) \to w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (w - r, w + r)$
50	47 48 49	syl2an	$⊢ ((A \in topGen (ran (.)) \land w \in A) \land r \in ℝ^{+}) \to w ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (w - r, w + r)$
51	50	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)$
52		2re	$⊢ 2 \in ℝ$
53		1lt2	$⊢ 1 < 2$
54		expnlbnd	$⊢ (r \in ℝ^{+} \land 2 \in ℝ \land 1 < 2) \to \exists n \in ℕ \frac{1}{2^{n}} < r$
55	52 53 54	mp3an23	$⊢ r \in ℝ^{+} \to \exists n \in ℕ \frac{1}{2^{n}} < r$
56	55	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$
57	47	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 ℝ$
58		2nn	$⊢ 2 \in ℕ$
59		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
60	59	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}$
61		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
62	58 60 61	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 ℕ$
63	62	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 ℝ$
64	57 63	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 ℝ$
65		fllelt	$⊢ w 2^{n} \in ℝ \to (⌊w 2^{n}⌋ \leq w 2^{n} \land w 2^{n} < ⌊w 2^{n}⌋ + 1)$
66	64 65	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)$
67	66	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}$
68		reflcl	$⊢ w 2^{n} \in ℝ \to ⌊w 2^{n}⌋ \in ℝ$
69	64 68	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 ℝ$
70	62	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}$
71		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})$
72	69 57 63 70 71	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})$
73	67 72	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$
74		peano2re	$⊢ ⌊w 2^{n}⌋ \in ℝ \to ⌊w 2^{n}⌋ + 1 \in ℝ$
75	69 74	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 ℝ$
76	75 62	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 ℝ$
77	66	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$
78		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}})$
79	57 75 63 70 78	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}})$
80	77 79	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}}$
81	57 76 80	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}}$
82	69 62	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 ℝ$
83		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}}))$
84	82 76 83	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}}))$
85	57 73 81 84	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}}]$
86	64	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 ℤ$
87	22	dyadval	$⊢ (⌊w 2^{n}⌋ \in ℤ \land n \in ℕ_{0}) \to ⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n = ⟨\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}⟩$
88	86 60 87	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}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n = ⟨\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}⟩$
89	88	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}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) = [.] (⟨\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}⟩)$
90		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}}⟩)$
91	89 90	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}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) = [\frac{⌊w 2^{n}⌋}{2^{n}}, \frac{⌊w 2^{n}⌋ + 1}{2^{n}}]$
92	85 91	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}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n)$
93		ffn	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) Fn (ℤ \times ℕ_{0})$
94	23 93	ax-mp	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) Fn (ℤ \times ℕ_{0})$
95		fnovrn	$⊢ ((x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) Fn (ℤ \times ℕ_{0}) \land ⌊w 2^{n}⌋ \in ℤ \land n \in ℕ_{0}) \to ⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
96	94 95	mp3an1	$⊢ (⌊w 2^{n}⌋ \in ℤ \land n \in ℕ_{0}) \to ⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
97	86 60 96	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}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
98		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 ℝ^{+}$
99	98	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 ℝ$
100	57 99	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 ℝ$
101	100	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 ℝ^{*}$
102	57 99	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 ℝ$
103	102	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 ℝ^{*}$
104	82 99	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 ℝ$
105	69	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 ℂ$
106		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 ℂ$
107	63	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 ℂ$
108	62	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$
109	105 106 107 108	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}})$
110	62	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 ℝ$
111		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$
112	110 99 82 111	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$
113	109 112	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$
114	57 76 104 80 113	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$
115	57 99 82	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)$
116	114 115	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}}$
117	57 110	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 ℝ$
118	82 57 110 73	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}})$
119	109 118	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}})$
120	110 99 57 111	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$
121	76 117 102 119 120	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$
122		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)$
123	101 103 116 121 122	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)$
124	91 123	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}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) \subseteq (w - r, w + r)$
125		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$
126	124 125	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}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) \subseteq A$
127		fveq2	$⊢ z = ⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \to [.] (z) = [.] (⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n)$
128	127	sseq1d	$⊢ z = ⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \to ([.] (z) \subseteq A \leftrightarrow [.] (⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) \subseteq A)$
129	128	elrab	$⊢ ⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \in \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} \leftrightarrow (⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \land [.] (⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) \subseteq A)$
130	97 126 129	sylanbrc	$⊢ (((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}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \in \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}$
131		funfvima2	$⊢ (Fun [.] \land \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} \subseteq dom [.]) \to (⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \in \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} \to [.] (⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) \in [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}])$
132	12 32 131	mp2an	$⊢ ⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n \in \{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\} \to [.] (⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) \in [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}]$
133	130 132	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}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) \in [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}]$
134		elunii	$⊢ (w \in [.] (⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) \land [.] (⌊w 2^{n}⌋ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) n) \in [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}]) \to w \in ⋃ [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}]$
135	92 133 134	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 (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}]$
136	56 135	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 (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}]$
137	136	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 (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}])$
138	51 137	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 (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}])$
139	138	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 (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}])$
140	43 139	mpd	$⊢ (A \in topGen (ran (.)) \land w \in A) \to w \in ⋃ [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}]$
141	37 140	eqelssd	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{z \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (z) \subseteq A\}] = A$

Metamath Proof Explorer

Theorem opnmbllem0

Proof