sxbrsigalem1

Description: The Borel algebra on ( RR X. RR ) is a subset of the sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ) . This is a step of the proof of Proposition 1.1.5 of Cohn p. 4. (Contributed by Thierry Arnoux, 17-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	sxbrsigalem1	$⊢ 𝛔 (J \times_{t} J) \subseteq 𝛔 (ran R)$

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	1 2 3	dya2iocucvr	$⊢ ⋃ ran R = ℝ^{2}$
5		retop	$⊢ topGen (ran (.)) \in Top$
6	1 5	eqeltri	$⊢ J \in Top$
7		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
8	1	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
9	7 8	eqtr4i	$⊢ ℝ = ⋃ J$
10	6 6 9 9	txunii	$⊢ ℝ^{2} = ⋃ (J \times_{t} J)$
11	4 10	eqtr2i	$⊢ ⋃ (J \times_{t} J) = ⋃ ran R$
12	1 2 3	dya2iocuni	$⊢ x \in (J \times_{t} J) \to \exists y \in 𝒫 ran R ⋃ y = x$
13		simpr	$⊢ (y \in 𝒫 ran R \land ⋃ y = x) \to ⋃ y = x$
14	1 2 3	dya2iocct	$⊢ ran R ≼ ω$
15		ctex	$⊢ ran R ≼ ω \to ran R \in V$
16	14 15	mp1i	$⊢ y \in 𝒫 ran R \to ran R \in V$
17		elpwi	$⊢ y \in 𝒫 ran R \to y \subseteq ran R$
18		ssct	$⊢ (y \subseteq ran R \land ran R ≼ ω) \to y ≼ ω$
19	17 14 18	sylancl	$⊢ y \in 𝒫 ran R \to y ≼ ω$
20		elsigagen2	$⊢ (ran R \in V \land y \subseteq ran R \land y ≼ ω) \to ⋃ y \in 𝛔 (ran R)$
21	16 17 19 20	syl3anc	$⊢ y \in 𝒫 ran R \to ⋃ y \in 𝛔 (ran R)$
22	21	adantr	$⊢ (y \in 𝒫 ran R \land ⋃ y = x) \to ⋃ y \in 𝛔 (ran R)$
23	13 22	eqeltrrd	$⊢ (y \in 𝒫 ran R \land ⋃ y = x) \to x \in 𝛔 (ran R)$
24	23	rexlimiva	$⊢ \exists y \in 𝒫 ran R ⋃ y = x \to x \in 𝛔 (ran R)$
25	12 24	syl	$⊢ x \in (J \times_{t} J) \to x \in 𝛔 (ran R)$
26	25	ssriv	$⊢ J \times_{t} J \subseteq 𝛔 (ran R)$
27	14 15	ax-mp	$⊢ ran R \in V$
28		sigagenss2	$⊢ (⋃ (J \times_{t} J) = ⋃ ran R \land J \times_{t} J \subseteq 𝛔 (ran R) \land ran R \in V) \to 𝛔 (J \times_{t} J) \subseteq 𝛔 (ran R)$
29	11 26 27 28	mp3an	$⊢ 𝛔 (J \times_{t} J) \subseteq 𝛔 (ran R)$

Metamath Proof Explorer

Theorem sxbrsigalem1

Proof