dya2iocucvr

Description: The dyadic rectangular set collection covers ( RR X. RR ) . (Contributed by Thierry Arnoux, 18-Sep-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}}))$
	dya2ioc.2	$⊢ R = (u \in ran I, v \in ran I ⟼ u \times v)$
Assertion	dya2iocucvr	$⊢ ⋃ ran R = ℝ^{2}$

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		dya2ioc.2	$⊢ R = (u \in ran I, v \in ran I ⟼ u \times v)$
4		unissb	$⊢ ⋃ ran R \subseteq ℝ^{2} \leftrightarrow \forall d \in ran R d \subseteq ℝ^{2}$
5		vex	$⊢ u \in V$
6		vex	$⊢ v \in V$
7	5 6	xpex	$⊢ u \times v \in V$
8	3 7	elrnmpo	$⊢ d \in ran R \leftrightarrow \exists u \in ran I \exists v \in ran I d = u \times v$
9		simpr	$⊢ ((u \in ran I \land v \in ran I) \land d = u \times v) \to d = u \times v$
10		pwssb	$⊢ ran I \subseteq 𝒫 ℝ \leftrightarrow \forall d \in ran I d \subseteq ℝ$
11		ovex	$⊢ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \in V$
12	2 11	elrnmpo	$⊢ d \in ran I \leftrightarrow \exists x \in ℤ \exists n \in ℤ d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
13		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}})$
14		simpll	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to x \in ℤ$
15	14	zred	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to x \in ℝ$
16		2re	$⊢ 2 \in ℝ$
17	16	a1i	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to 2 \in ℝ$
18		2ne0	$⊢ 2 \neq 0$
19	18	a1i	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to 2 \neq 0$
20		simplr	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to n \in ℤ$
21	17 19 20	reexpclzd	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to 2^{n} \in ℝ$
22		2cnd	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to 2 \in ℂ$
23	22 19 20	expne0d	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to 2^{n} \neq 0$
24	15 21 23	redivcld	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to \frac{x}{2^{n}} \in ℝ$
25		1red	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to 1 \in ℝ$
26	15 25	readdcld	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to x + 1 \in ℝ$
27	26 21 23	redivcld	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to \frac{x + 1}{2^{n}} \in ℝ$
28	27	rexrd	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to \frac{x + 1}{2^{n}} \in ℝ^{*}$
29		icossre	$⊢ (\frac{x}{2^{n}} \in ℝ \land \frac{x + 1}{2^{n}} \in ℝ^{*}) \to [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \subseteq ℝ$
30	24 28 29	syl2anc	$⊢ ((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}}) \subseteq ℝ$
31	13 30	eqsstrd	$⊢ ((x \in ℤ \land n \in ℤ) \land d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to d \subseteq ℝ$
32	31	ex	$⊢ (x \in ℤ \land n \in ℤ) \to (d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \to d \subseteq ℝ)$
33	32	rexlimivv	$⊢ \exists x \in ℤ \exists n \in ℤ d = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \to d \subseteq ℝ$
34	12 33	sylbi	$⊢ d \in ran I \to d \subseteq ℝ$
35	10 34	mprgbir	$⊢ ran I \subseteq 𝒫 ℝ$
36	35	sseli	$⊢ u \in ran I \to u \in 𝒫 ℝ$
37	36	elpwid	$⊢ u \in ran I \to u \subseteq ℝ$
38	35	sseli	$⊢ v \in ran I \to v \in 𝒫 ℝ$
39	38	elpwid	$⊢ v \in ran I \to v \subseteq ℝ$
40		xpss12	$⊢ (u \subseteq ℝ \land v \subseteq ℝ) \to u \times v \subseteq ℝ^{2}$
41	37 39 40	syl2an	$⊢ (u \in ran I \land v \in ran I) \to u \times v \subseteq ℝ^{2}$
42	41	adantr	$⊢ ((u \in ran I \land v \in ran I) \land d = u \times v) \to u \times v \subseteq ℝ^{2}$
43	9 42	eqsstrd	$⊢ ((u \in ran I \land v \in ran I) \land d = u \times v) \to d \subseteq ℝ^{2}$
44	43	ex	$⊢ (u \in ran I \land v \in ran I) \to (d = u \times v \to d \subseteq ℝ^{2})$
45	44	rexlimivv	$⊢ \exists u \in ran I \exists v \in ran I d = u \times v \to d \subseteq ℝ^{2}$
46	8 45	sylbi	$⊢ d \in ran R \to d \subseteq ℝ^{2}$
47	4 46	mprgbir	$⊢ ⋃ ran R \subseteq ℝ^{2}$
48		retop	$⊢ topGen (ran (.)) \in Top$
49	1 48	eqeltri	$⊢ J \in Top$
50	49 49	txtopi	$⊢ J \times_{t} J \in Top$
51		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
52	1	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
53	51 52	eqtr4i	$⊢ ℝ = ⋃ J$
54	49 49 53 53	txunii	$⊢ ℝ^{2} = ⋃ (J \times_{t} J)$
55	54	topopn	$⊢ J \times_{t} J \in Top \to ℝ^{2} \in (J \times_{t} J)$
56	1 2 3	dya2iocuni	$⊢ ℝ^{2} \in (J \times_{t} J) \to \exists c \in 𝒫 ran R ⋃ c = ℝ^{2}$
57	50 55 56	mp2b	$⊢ \exists c \in 𝒫 ran R ⋃ c = ℝ^{2}$
58		simpr	$⊢ (c \in 𝒫 ran R \land ⋃ c = ℝ^{2}) \to ⋃ c = ℝ^{2}$
59		elpwi	$⊢ c \in 𝒫 ran R \to c \subseteq ran R$
60	59	adantr	$⊢ (c \in 𝒫 ran R \land ⋃ c = ℝ^{2}) \to c \subseteq ran R$
61	60	unissd	$⊢ (c \in 𝒫 ran R \land ⋃ c = ℝ^{2}) \to ⋃ c \subseteq ⋃ ran R$
62	58 61	eqsstrrd	$⊢ (c \in 𝒫 ran R \land ⋃ c = ℝ^{2}) \to ℝ^{2} \subseteq ⋃ ran R$
63	62	rexlimiva	$⊢ \exists c \in 𝒫 ran R ⋃ c = ℝ^{2} \to ℝ^{2} \subseteq ⋃ ran R$
64	57 63	ax-mp	$⊢ ℝ^{2} \subseteq ⋃ ran R$
65	47 64	eqssi	$⊢ ⋃ ran R = ℝ^{2}$

Metamath Proof Explorer

Theorem dya2iocucvr

Proof