sxbrsigalem2

Description: The sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ) is a subset of the sigma-algebra generated by the closed half-spaces of ( RR X. RR ) . The proof goes by noting the fact that the dyadic rectangles are intersections of a 'vertical band' and an 'horizontal band', which themselves are differences of closed half-spaces. (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	sxbrsigalem2	$⊢ 𝛔 (ran R) \subseteq 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$

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		sxbrsigalem0	$⊢ ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) = ℝ^{2}$
6	4 5	eqtr4i	$⊢ ⋃ ran R = ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
7		vex	$⊢ u \in V$
8		vex	$⊢ v \in V$
9	7 8	xpex	$⊢ u \times v \in V$
10	3 9	elrnmpo	$⊢ d \in ran R \leftrightarrow \exists u \in ran I \exists v \in ran I d = u \times v$
11		simpr	$⊢ ((u \in ran I \land v \in ran I) \land d = u \times v) \to d = u \times v$
12	1 2	dya2icobrsiga	$⊢ ran I \subseteq 𝔅_{ℝ}$
13		brsigasspwrn	$⊢ 𝔅_{ℝ} \subseteq 𝒫 ℝ$
14	12 13	sstri	$⊢ ran I \subseteq 𝒫 ℝ$
15	14	sseli	$⊢ u \in ran I \to u \in 𝒫 ℝ$
16	15	elpwid	$⊢ u \in ran I \to u \subseteq ℝ$
17	14	sseli	$⊢ v \in ran I \to v \in 𝒫 ℝ$
18	17	elpwid	$⊢ v \in ran I \to v \subseteq ℝ$
19		xpinpreima2	$⊢ (u \subseteq ℝ \land v \subseteq ℝ) \to u \times v = {({1^{st} ↾}_{ℝ^{2}})}^{-1} [u] \cap {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [v]$
20	16 18 19	syl2an	$⊢ (u \in ran I \land v \in ran I) \to u \times v = {({1^{st} ↾}_{ℝ^{2}})}^{-1} [u] \cap {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [v]$
21		reex	$⊢ ℝ \in V$
22	21	mptex	$⊢ (e \in ℝ ⟼ [e, +∞) \times ℝ) \in V$
23	22	rnex	$⊢ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \in V$
24	21	mptex	$⊢ (f \in ℝ ⟼ ℝ \times [f, +∞)) \in V$
25	24	rnex	$⊢ ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \in V$
26	23 25	unex	$⊢ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \in V$
27	26	a1i	$⊢ ⊤ \to ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \in V$
28	27	sgsiga	$⊢ ⊤ \to 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \in ⋃ ran sigAlgebra$
29	28	mptru	$⊢ 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \in ⋃ ran sigAlgebra$
30	29	a1i	$⊢ (u \in ran I \land v \in ran I) \to 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \in ⋃ ran sigAlgebra$
31		1stpreima	$⊢ u \subseteq ℝ \to {({1^{st} ↾}_{ℝ^{2}})}^{-1} [u] = u \times ℝ$
32	16 31	syl	$⊢ u \in ran I \to {({1^{st} ↾}_{ℝ^{2}})}^{-1} [u] = u \times ℝ$
33		ovex	$⊢ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \in V$
34	2 33	elrnmpo	$⊢ u \in ran I \leftrightarrow \exists x \in ℤ \exists n \in ℤ u = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
35		simpr	$⊢ ((x \in ℤ \land n \in ℤ) \land u = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to u = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
36	35	xpeq1d	$⊢ ((x \in ℤ \land n \in ℤ) \land u = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to u \times ℝ = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \times ℝ$
37		difxp1	$⊢ ([\frac{x}{2^{n}}, +∞) ∖ [\frac{x + 1}{2^{n}}, +∞)) \times ℝ = ([\frac{x}{2^{n}}, +∞) \times ℝ) ∖ ([\frac{x + 1}{2^{n}}, +∞) \times ℝ)$
38		simpl	$⊢ (x \in ℤ \land n \in ℤ) \to x \in ℤ$
39	38	zred	$⊢ (x \in ℤ \land n \in ℤ) \to x \in ℝ$
40		2rp	$⊢ 2 \in ℝ^{+}$
41	40	a1i	$⊢ (x \in ℤ \land n \in ℤ) \to 2 \in ℝ^{+}$
42		simpr	$⊢ (x \in ℤ \land n \in ℤ) \to n \in ℤ$
43	41 42	rpexpcld	$⊢ (x \in ℤ \land n \in ℤ) \to 2^{n} \in ℝ^{+}$
44	39 43	rerpdivcld	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x}{2^{n}} \in ℝ$
45	44	rexrd	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x}{2^{n}} \in ℝ^{*}$
46		1red	$⊢ (x \in ℤ \land n \in ℤ) \to 1 \in ℝ$
47	39 46	readdcld	$⊢ (x \in ℤ \land n \in ℤ) \to x + 1 \in ℝ$
48	47 43	rerpdivcld	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x + 1}{2^{n}} \in ℝ$
49	48	rexrd	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x + 1}{2^{n}} \in ℝ^{*}$
50		pnfxr	$⊢ +∞ \in ℝ^{*}$
51	50	a1i	$⊢ (x \in ℤ \land n \in ℤ) \to +∞ \in ℝ^{*}$
52	39	lep1d	$⊢ (x \in ℤ \land n \in ℤ) \to x \leq x + 1$
53	39 47 43 52	lediv1dd	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x}{2^{n}} \leq \frac{x + 1}{2^{n}}$
54		pnfge	$⊢ \frac{x + 1}{2^{n}} \in ℝ^{*} \to \frac{x + 1}{2^{n}} \leq +∞$
55	49 54	syl	$⊢ (x \in ℤ \land n \in ℤ) \to \frac{x + 1}{2^{n}} \leq +∞$
56		difico	$⊢ ((\frac{x}{2^{n}} \in ℝ^{} \land \frac{x + 1}{2^{n}} \in ℝ^{} \land +∞ \in ℝ^{*}) \land (\frac{x}{2^{n}} \leq \frac{x + 1}{2^{n}} \land \frac{x + 1}{2^{n}} \leq +∞)) \to [\frac{x}{2^{n}}, +∞) ∖ [\frac{x + 1}{2^{n}}, +∞) = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
57	45 49 51 53 55 56	syl32anc	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x}{2^{n}}, +∞) ∖ [\frac{x + 1}{2^{n}}, +∞) = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
58	57	xpeq1d	$⊢ (x \in ℤ \land n \in ℤ) \to ([\frac{x}{2^{n}}, +∞) ∖ [\frac{x + 1}{2^{n}}, +∞)) \times ℝ = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \times ℝ$
59	37 58	syl5reqr	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \times ℝ = ([\frac{x}{2^{n}}, +∞) \times ℝ) ∖ ([\frac{x + 1}{2^{n}}, +∞) \times ℝ)$
60	29	a1i	$⊢ (x \in ℤ \land n \in ℤ) \to 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \in ⋃ ran sigAlgebra$
61		ssun1	$⊢ ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \subseteq ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
62		eqid	$⊢ [\frac{x}{2^{n}}, +∞) \times ℝ = [\frac{x}{2^{n}}, +∞) \times ℝ$
63		oveq1	$⊢ e = \frac{x}{2^{n}} \to [e, +∞) = [\frac{x}{2^{n}}, +∞)$
64	63	xpeq1d	$⊢ e = \frac{x}{2^{n}} \to [e, +∞) \times ℝ = [\frac{x}{2^{n}}, +∞) \times ℝ$
65	64	rspceeqv	$⊢ (\frac{x}{2^{n}} \in ℝ \land [\frac{x}{2^{n}}, +∞) \times ℝ = [\frac{x}{2^{n}}, +∞) \times ℝ) \to \exists e \in ℝ [\frac{x}{2^{n}}, +∞) \times ℝ = [e, +∞) \times ℝ$
66	44 62 65	sylancl	$⊢ (x \in ℤ \land n \in ℤ) \to \exists e \in ℝ [\frac{x}{2^{n}}, +∞) \times ℝ = [e, +∞) \times ℝ$
67		eqid	$⊢ (e \in ℝ ⟼ [e, +∞) \times ℝ) = (e \in ℝ ⟼ [e, +∞) \times ℝ)$
68		ovex	$⊢ [e, +∞) \in V$
69	68 21	xpex	$⊢ [e, +∞) \times ℝ \in V$
70	67 69	elrnmpti	$⊢ [\frac{x}{2^{n}}, +∞) \times ℝ \in ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \leftrightarrow \exists e \in ℝ [\frac{x}{2^{n}}, +∞) \times ℝ = [e, +∞) \times ℝ$
71	66 70	sylibr	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x}{2^{n}}, +∞) \times ℝ \in ran (e \in ℝ ⟼ [e, +∞) \times ℝ)$
72	61 71	sseldi	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x}{2^{n}}, +∞) \times ℝ \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
73		elsigagen	$⊢ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \in V \land [\frac{x}{2^{n}}, +∞) \times ℝ \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))) \to [\frac{x}{2^{n}}, +∞) \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
74	26 72 73	sylancr	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x}{2^{n}}, +∞) \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
75		eqid	$⊢ [\frac{x + 1}{2^{n}}, +∞) \times ℝ = [\frac{x + 1}{2^{n}}, +∞) \times ℝ$
76		oveq1	$⊢ e = \frac{x + 1}{2^{n}} \to [e, +∞) = [\frac{x + 1}{2^{n}}, +∞)$
77	76	xpeq1d	$⊢ e = \frac{x + 1}{2^{n}} \to [e, +∞) \times ℝ = [\frac{x + 1}{2^{n}}, +∞) \times ℝ$
78	77	rspceeqv	$⊢ (\frac{x + 1}{2^{n}} \in ℝ \land [\frac{x + 1}{2^{n}}, +∞) \times ℝ = [\frac{x + 1}{2^{n}}, +∞) \times ℝ) \to \exists e \in ℝ [\frac{x + 1}{2^{n}}, +∞) \times ℝ = [e, +∞) \times ℝ$
79	48 75 78	sylancl	$⊢ (x \in ℤ \land n \in ℤ) \to \exists e \in ℝ [\frac{x + 1}{2^{n}}, +∞) \times ℝ = [e, +∞) \times ℝ$
80	67 69	elrnmpti	$⊢ [\frac{x + 1}{2^{n}}, +∞) \times ℝ \in ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \leftrightarrow \exists e \in ℝ [\frac{x + 1}{2^{n}}, +∞) \times ℝ = [e, +∞) \times ℝ$
81	79 80	sylibr	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x + 1}{2^{n}}, +∞) \times ℝ \in ran (e \in ℝ ⟼ [e, +∞) \times ℝ)$
82	61 81	sseldi	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x + 1}{2^{n}}, +∞) \times ℝ \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
83		elsigagen	$⊢ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \in V \land [\frac{x + 1}{2^{n}}, +∞) \times ℝ \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))) \to [\frac{x + 1}{2^{n}}, +∞) \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
84	26 82 83	sylancr	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x + 1}{2^{n}}, +∞) \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
85		difelsiga	$⊢ (𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \in ⋃ ran sigAlgebra \land [\frac{x}{2^{n}}, +∞) \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \land [\frac{x + 1}{2^{n}}, +∞) \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))) \to ([\frac{x}{2^{n}}, +∞) \times ℝ) ∖ ([\frac{x + 1}{2^{n}}, +∞) \times ℝ) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
86	60 74 84 85	syl3anc	$⊢ (x \in ℤ \land n \in ℤ) \to ([\frac{x}{2^{n}}, +∞) \times ℝ) ∖ ([\frac{x + 1}{2^{n}}, +∞) \times ℝ) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
87	59 86	eqeltrd	$⊢ (x \in ℤ \land n \in ℤ) \to [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
88	87	adantr	$⊢ ((x \in ℤ \land n \in ℤ) \land u = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
89	36 88	eqeltrd	$⊢ ((x \in ℤ \land n \in ℤ) \land u = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to u \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
90	89	ex	$⊢ (x \in ℤ \land n \in ℤ) \to (u = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \to u \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))))$
91	90	rexlimivv	$⊢ \exists x \in ℤ \exists n \in ℤ u = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \to u \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
92	34 91	sylbi	$⊢ u \in ran I \to u \times ℝ \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
93	32 92	eqeltrd	$⊢ u \in ran I \to {({1^{st} ↾}_{ℝ^{2}})}^{-1} [u] \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
94	93	adantr	$⊢ (u \in ran I \land v \in ran I) \to {({1^{st} ↾}_{ℝ^{2}})}^{-1} [u] \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
95		2ndpreima	$⊢ v \subseteq ℝ \to {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [v] = ℝ \times v$
96	18 95	syl	$⊢ v \in ran I \to {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [v] = ℝ \times v$
97	2 33	elrnmpo	$⊢ v \in ran I \leftrightarrow \exists x \in ℤ \exists n \in ℤ v = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
98		simpr	$⊢ ((x \in ℤ \land n \in ℤ) \land v = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to v = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
99	98	xpeq2d	$⊢ ((x \in ℤ \land n \in ℤ) \land v = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to ℝ \times v = ℝ \times [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
100		difxp2	$⊢ ℝ \times ([\frac{x}{2^{n}}, +∞) ∖ [\frac{x + 1}{2^{n}}, +∞)) = (ℝ \times [\frac{x}{2^{n}}, +∞)) ∖ (ℝ \times [\frac{x + 1}{2^{n}}, +∞))$
101	57	xpeq2d	$⊢ (x \in ℤ \land n \in ℤ) \to ℝ \times ([\frac{x}{2^{n}}, +∞) ∖ [\frac{x + 1}{2^{n}}, +∞)) = ℝ \times [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
102	100 101	syl5reqr	$⊢ (x \in ℤ \land n \in ℤ) \to ℝ \times [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) = (ℝ \times [\frac{x}{2^{n}}, +∞)) ∖ (ℝ \times [\frac{x + 1}{2^{n}}, +∞))$
103		ssun2	$⊢ ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \subseteq ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
104		eqid	$⊢ ℝ \times [\frac{x}{2^{n}}, +∞) = ℝ \times [\frac{x}{2^{n}}, +∞)$
105		oveq1	$⊢ f = \frac{x}{2^{n}} \to [f, +∞) = [\frac{x}{2^{n}}, +∞)$
106	105	xpeq2d	$⊢ f = \frac{x}{2^{n}} \to ℝ \times [f, +∞) = ℝ \times [\frac{x}{2^{n}}, +∞)$
107	106	rspceeqv	$⊢ (\frac{x}{2^{n}} \in ℝ \land ℝ \times [\frac{x}{2^{n}}, +∞) = ℝ \times [\frac{x}{2^{n}}, +∞)) \to \exists f \in ℝ ℝ \times [\frac{x}{2^{n}}, +∞) = ℝ \times [f, +∞)$
108	44 104 107	sylancl	$⊢ (x \in ℤ \land n \in ℤ) \to \exists f \in ℝ ℝ \times [\frac{x}{2^{n}}, +∞) = ℝ \times [f, +∞)$
109		eqid	$⊢ (f \in ℝ ⟼ ℝ \times [f, +∞)) = (f \in ℝ ⟼ ℝ \times [f, +∞))$
110		ovex	$⊢ [f, +∞) \in V$
111	21 110	xpex	$⊢ ℝ \times [f, +∞) \in V$
112	109 111	elrnmpti	$⊢ ℝ \times [\frac{x}{2^{n}}, +∞) \in ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \leftrightarrow \exists f \in ℝ ℝ \times [\frac{x}{2^{n}}, +∞) = ℝ \times [f, +∞)$
113	108 112	sylibr	$⊢ (x \in ℤ \land n \in ℤ) \to ℝ \times [\frac{x}{2^{n}}, +∞) \in ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
114	103 113	sseldi	$⊢ (x \in ℤ \land n \in ℤ) \to ℝ \times [\frac{x}{2^{n}}, +∞) \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
115		elsigagen	$⊢ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \in V \land ℝ \times [\frac{x}{2^{n}}, +∞) \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))) \to ℝ \times [\frac{x}{2^{n}}, +∞) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
116	26 114 115	sylancr	$⊢ (x \in ℤ \land n \in ℤ) \to ℝ \times [\frac{x}{2^{n}}, +∞) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
117		eqid	$⊢ ℝ \times [\frac{x + 1}{2^{n}}, +∞) = ℝ \times [\frac{x + 1}{2^{n}}, +∞)$
118		oveq1	$⊢ f = \frac{x + 1}{2^{n}} \to [f, +∞) = [\frac{x + 1}{2^{n}}, +∞)$
119	118	xpeq2d	$⊢ f = \frac{x + 1}{2^{n}} \to ℝ \times [f, +∞) = ℝ \times [\frac{x + 1}{2^{n}}, +∞)$
120	119	rspceeqv	$⊢ (\frac{x + 1}{2^{n}} \in ℝ \land ℝ \times [\frac{x + 1}{2^{n}}, +∞) = ℝ \times [\frac{x + 1}{2^{n}}, +∞)) \to \exists f \in ℝ ℝ \times [\frac{x + 1}{2^{n}}, +∞) = ℝ \times [f, +∞)$
121	48 117 120	sylancl	$⊢ (x \in ℤ \land n \in ℤ) \to \exists f \in ℝ ℝ \times [\frac{x + 1}{2^{n}}, +∞) = ℝ \times [f, +∞)$
122	109 111	elrnmpti	$⊢ ℝ \times [\frac{x + 1}{2^{n}}, +∞) \in ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \leftrightarrow \exists f \in ℝ ℝ \times [\frac{x + 1}{2^{n}}, +∞) = ℝ \times [f, +∞)$
123	121 122	sylibr	$⊢ (x \in ℤ \land n \in ℤ) \to ℝ \times [\frac{x + 1}{2^{n}}, +∞) \in ran (f \in ℝ ⟼ ℝ \times [f, +∞))$
124	103 123	sseldi	$⊢ (x \in ℤ \land n \in ℤ) \to ℝ \times [\frac{x + 1}{2^{n}}, +∞) \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
125		elsigagen	$⊢ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \in V \land ℝ \times [\frac{x + 1}{2^{n}}, +∞) \in (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))) \to ℝ \times [\frac{x + 1}{2^{n}}, +∞) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
126	26 124 125	sylancr	$⊢ (x \in ℤ \land n \in ℤ) \to ℝ \times [\frac{x + 1}{2^{n}}, +∞) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
127		difelsiga	$⊢ (𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \in ⋃ ran sigAlgebra \land ℝ \times [\frac{x}{2^{n}}, +∞) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \land ℝ \times [\frac{x + 1}{2^{n}}, +∞) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))) \to (ℝ \times [\frac{x}{2^{n}}, +∞)) ∖ (ℝ \times [\frac{x + 1}{2^{n}}, +∞)) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
128	60 116 126 127	syl3anc	$⊢ (x \in ℤ \land n \in ℤ) \to (ℝ \times [\frac{x}{2^{n}}, +∞)) ∖ (ℝ \times [\frac{x + 1}{2^{n}}, +∞)) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
129	102 128	eqeltrd	$⊢ (x \in ℤ \land n \in ℤ) \to ℝ \times [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
130	129	adantr	$⊢ ((x \in ℤ \land n \in ℤ) \land v = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to ℝ \times [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
131	99 130	eqeltrd	$⊢ ((x \in ℤ \land n \in ℤ) \land v = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \to ℝ \times v \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
132	131	ex	$⊢ (x \in ℤ \land n \in ℤ) \to (v = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \to ℝ \times v \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))))$
133	132	rexlimivv	$⊢ \exists x \in ℤ \exists n \in ℤ v = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}) \to ℝ \times v \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
134	97 133	sylbi	$⊢ v \in ran I \to ℝ \times v \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
135	96 134	eqeltrd	$⊢ v \in ran I \to {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [v] \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
136	135	adantl	$⊢ (u \in ran I \land v \in ran I) \to {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [v] \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
137		inelsiga	$⊢ (𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \in ⋃ ran sigAlgebra \land {({1^{st} ↾}_{ℝ^{2}})}^{-1} [u] \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \land {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [v] \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))) \to {({1^{st} ↾}_{ℝ^{2}})}^{-1} [u] \cap {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [v] \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
138	30 94 136 137	syl3anc	$⊢ (u \in ran I \land v \in ran I) \to {({1^{st} ↾}_{ℝ^{2}})}^{-1} [u] \cap {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [v] \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
139	20 138	eqeltrd	$⊢ (u \in ran I \land v \in ran I) \to u \times v \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
140	139	adantr	$⊢ ((u \in ran I \land v \in ran I) \land d = u \times v) \to u \times v \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
141	11 140	eqeltrd	$⊢ ((u \in ran I \land v \in ran I) \land d = u \times v) \to d \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
142	141	ex	$⊢ (u \in ran I \land v \in ran I) \to (d = u \times v \to d \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))))$
143	142	rexlimivv	$⊢ \exists u \in ran I \exists v \in ran I d = u \times v \to d \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
144	10 143	sylbi	$⊢ d \in ran R \to d \in 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
145	144	ssriv	$⊢ ran R \subseteq 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
146		sigagenss2	$⊢ (⋃ ran R = ⋃ (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \land ran R \subseteq 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞))) \land ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)) \in V) \to 𝛔 (ran R) \subseteq 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$
147	6 145 26 146	mp3an	$⊢ 𝛔 (ran R) \subseteq 𝛔 (ran (e \in ℝ ⟼ [e, +∞) \times ℝ) \cup ran (f \in ℝ ⟼ ℝ \times [f, +∞)))$

Metamath Proof Explorer

Theorem sxbrsigalem2

Proof