dya2icobrsiga

Description: Dyadic intervals are Borel sets of RR . (Contributed by Thierry Arnoux, 22-Sep-2017) (Revised by Thierry Arnoux, 13-Oct-2017)

	Ref	Expression
Hypotheses	sxbrsiga.0	$⊢ J = topGen (ran (.))$
	dya2ioc.1	$⊢ I = (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
Assertion	dya2icobrsiga	$⊢ ran I \subseteq 𝔅_{ℝ}$

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	$⊢ J = topGen (ran (.))$
2		dya2ioc.1	$⊢ I = (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
3		ovex	$⊢ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \in V$
4	2 3	elrnmpo	$⊢ d \in ran I \leftrightarrow \exists x \in ℤ \exists n \in ℤ d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
5		simpr	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
6		mnfxr	$⊢ −∞ \in ℝ^{*}$
7	6	a1i	$⊢ (x \in ℤ \land n \in ℤ) \to −∞ \in ℝ^{*}$
8		simpl	$⊢ (x \in ℤ \land n \in ℤ) \to x \in ℤ$
9	8	zred	$⊢ (x \in ℤ \land n \in ℤ) \to x \in ℝ$
10		2rp	$⊢ 2 \in ℝ^{+}$
11	10	a1i	$⊢ (x \in ℤ \land n \in ℤ) \to 2 \in ℝ^{+}$
12		simpr	$⊢ (x \in ℤ \land n \in ℤ) \to n \in ℤ$
13	11 12	rpexpcld	$⊢ (x \in ℤ \land n \in ℤ) \to 2^{n} \in ℝ^{+}$
14	9 13	rerpdivcld	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x}{2^{n}} \in ℝ$
15	14	rexrd	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x}{2^{n}} \in ℝ^{*}$
16		1red	$⊢ (x \in ℤ \land n \in ℤ) \to 1 \in ℝ$
17	9 16	readdcld	$⊢ (x \in ℤ \land n \in ℤ) \to x + 1 \in ℝ$
18	17 13	rerpdivcld	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x + 1}{2^{n}} \in ℝ$
19	18	rexrd	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x + 1}{2^{n}} \in ℝ^{*}$
20		mnflt	$⊢ \frac{x}{2^{n}} \in ℝ \to −∞ < \frac{x}{2^{n}}$
21	14 20	syl	$⊢ (x \in ℤ \land n \in ℤ) \to −∞ < \frac{x}{2^{n}}$
22		difioo	$⊢ ((−∞ \in ℝ^{} \land \frac{x}{2^{n}} \in ℝ^{} \land \frac{x + 1}{2^{n}} \in ℝ^{*}) \land −∞ < \frac{x}{2^{n}}) \to (−∞, \frac{x + 1}{2^{n}}) ∖ (−∞, \frac{x}{2^{n}}) = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
23	7 15 19 21 22	syl31anc	$⊢ (x \in ℤ \land n \in ℤ) \to (−∞, \frac{x + 1}{2^{n}}) ∖ (−∞, \frac{x}{2^{n}}) = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
24		brsigarn	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ)$
25		elrnsiga	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ) \to 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
26	24 25	ax-mp	$⊢ 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
27		retop	$⊢ topGen (ran (.)) \in Top$
28		iooretop	$⊢ (−∞, \frac{x + 1}{2^{n}}) \in topGen (ran (.))$
29		elsigagen	$⊢ (topGen (ran (.)) \in Top \land (−∞, \frac{x + 1}{2^{n}}) \in topGen (ran (.))) \to (−∞, \frac{x + 1}{2^{n}}) \in 𝛔 (topGen (ran (.)))$
30	27 28 29	mp2an	$⊢ (−∞, \frac{x + 1}{2^{n}}) \in 𝛔 (topGen (ran (.)))$
31		df-brsiga	$⊢ 𝔅_{ℝ} = 𝛔 (topGen (ran (.)))$
32	30 31	eleqtrri	$⊢ (−∞, \frac{x + 1}{2^{n}}) \in 𝔅_{ℝ}$
33		iooretop	$⊢ (−∞, \frac{x}{2^{n}}) \in topGen (ran (.))$
34		elsigagen	$⊢ (topGen (ran (.)) \in Top \land (−∞, \frac{x}{2^{n}}) \in topGen (ran (.))) \to (−∞, \frac{x}{2^{n}}) \in 𝛔 (topGen (ran (.)))$
35	27 33 34	mp2an	$⊢ (−∞, \frac{x}{2^{n}}) \in 𝛔 (topGen (ran (.)))$
36	35 31	eleqtrri	$⊢ (−∞, \frac{x}{2^{n}}) \in 𝔅_{ℝ}$
37		difelsiga	$⊢ (𝔅_{ℝ} \in ⋃ ran sigAlgebra \land (−∞, \frac{x + 1}{2^{n}}) \in 𝔅_{ℝ} \land (−∞, \frac{x}{2^{n}}) \in 𝔅_{ℝ}) \to (−∞, \frac{x + 1}{2^{n}}) ∖ (−∞, \frac{x}{2^{n}}) \in 𝔅_{ℝ}$
38	26 32 36 37	mp3an	$⊢ (−∞, \frac{x + 1}{2^{n}}) ∖ (−∞, \frac{x}{2^{n}}) \in 𝔅_{ℝ}$
39	23 38	eqeltrrdi	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \in 𝔅_{ℝ}$
40	39	adantr	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \in 𝔅_{ℝ}$
41	5 40	eqeltrd	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to d \in 𝔅_{ℝ}$
42	41	ex	$⊢ (x \in ℤ \land n \in ℤ) \to (d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \to d \in 𝔅_{ℝ})$
43	42	rexlimivv	$⊢ \exists x \in ℤ \exists n \in ℤ d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \to d \in 𝔅_{ℝ}$
44	4 43	sylbi	$⊢ d \in ran I \to d \in 𝔅_{ℝ}$
45	44	ssriv	$⊢ ran I \subseteq 𝔅_{ℝ}$

Metamath Proof Explorer

Theorem dya2icobrsiga

Proof