sxbrsigalem2 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sxbrsigalem2		Structured version Visualization version GIF version

Theorem sxbrsigalem2 31544

Description: The sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of (ℝ × ℝ) is a subset of the sigma-algebra generated by the closed half-spaces of (ℝ × ℝ). 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.)

**Hypotheses**
Ref	Expression
sxbrsiga.0	⊢ 𝐽 = (topGen‘ran (,))
dya2ioc.1	⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
dya2ioc.2	⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))

**Assertion**
Ref	Expression
sxbrsigalem2	⊢ (sigaGen‘ran 𝑅) ⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))

Distinct variable groups: 𝑥,𝑛 𝑥,𝐼 𝑣,𝑢,𝐼,𝑥 𝑢,𝑛,𝑣 𝑅,𝑛,𝑥 𝑥,𝐽 𝑒,𝑓,𝑛,𝑢,𝑣,𝑥 Allowed substitution hints: 𝑅(𝑣,𝑢,𝑒,𝑓) 𝐼(𝑒,𝑓,𝑛) 𝐽(𝑣,𝑢,𝑒,𝑓,𝑛)

Proof of Theorem sxbrsigalem2 Dummy variable 𝑑 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sxbrsiga.0	. . . 4 ⊢ 𝐽 = (topGen‘ran (,))
2		dya2ioc.1	. . . 4 ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
3		dya2ioc.2	. . . 4 ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))
4	1, 2, 3	dya2iocucvr 31542	. . 3 ⊢ ∪ ran 𝑅 = (ℝ × ℝ)
5		sxbrsigalem0 31529	. . 3 ⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) = (ℝ × ℝ)
6	4, 5	eqtr4i 2847	. 2 ⊢ ∪ ran 𝑅 = ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))
7		vex 3497	. . . . . 6 ⊢ 𝑢 ∈ V
8		vex 3497	. . . . . 6 ⊢ 𝑣 ∈ V
9	7, 8	xpex 7476	. . . . 5 ⊢ (𝑢 × 𝑣) ∈ V
10	3, 9	elrnmpo 7287	. . . 4 ⊢ (𝑑 ∈ ran 𝑅 ↔ ∃𝑢 ∈ ran 𝐼∃𝑣 ∈ ran 𝐼 𝑑 = (𝑢 × 𝑣))
11		simpr 487	. . . . . . 7 ⊢ (((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) ∧ 𝑑 = (𝑢 × 𝑣)) → 𝑑 = (𝑢 × 𝑣))
12	1, 2	dya2icobrsiga 31534	. . . . . . . . . . . . 13 ⊢ ran 𝐼 ⊆ 𝔅_ℝ
13		brsigasspwrn 31444	. . . . . . . . . . . . 13 ⊢ 𝔅_ℝ ⊆ 𝒫 ℝ
14	12, 13	sstri 3976	. . . . . . . . . . . 12 ⊢ ran 𝐼 ⊆ 𝒫 ℝ
15	14	sseli 3963	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ran 𝐼 → 𝑢 ∈ 𝒫 ℝ)
16	15	elpwid 4550	. . . . . . . . . 10 ⊢ (𝑢 ∈ ran 𝐼 → 𝑢 ⊆ ℝ)
17	14	sseli 3963	. . . . . . . . . . 11 ⊢ (𝑣 ∈ ran 𝐼 → 𝑣 ∈ 𝒫 ℝ)
18	17	elpwid 4550	. . . . . . . . . 10 ⊢ (𝑣 ∈ ran 𝐼 → 𝑣 ⊆ ℝ)
19		xpinpreima2 31150	. . . . . . . . . 10 ⊢ ((𝑢 ⊆ ℝ ∧ 𝑣 ⊆ ℝ) → (𝑢 × 𝑣) = ((^◡(1^st ↾ (ℝ × ℝ)) “ 𝑢) ∩ (^◡(2^nd ↾ (ℝ × ℝ)) “ 𝑣)))
20	16, 18, 19	syl2an 597	. . . . . . . . 9 ⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (𝑢 × 𝑣) = ((^◡(1^st ↾ (ℝ × ℝ)) “ 𝑢) ∩ (^◡(2^nd ↾ (ℝ × ℝ)) “ 𝑣)))
21		reex 10628	. . . . . . . . . . . . . . . . 17 ⊢ ℝ ∈ V
22	21	mptex 6986	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∈ V
23	22	rnex 7617	. . . . . . . . . . . . . . 15 ⊢ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∈ V
24	21	mptex 6986	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))) ∈ V
25	24	rnex 7617	. . . . . . . . . . . . . . 15 ⊢ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))) ∈ V
26	23, 25	unex 7469	. . . . . . . . . . . . . 14 ⊢ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V
27	26	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V)
28	27	sgsiga 31401	. . . . . . . . . . . 12 ⊢ (⊤ → (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra)
29	28	mptru 1544	. . . . . . . . . . 11 ⊢ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra
30	29	a1i 11	. . . . . . . . . 10 ⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra)
31		1stpreima 30442	. . . . . . . . . . . . 13 ⊢ (𝑢 ⊆ ℝ → (^◡(1^st ↾ (ℝ × ℝ)) “ 𝑢) = (𝑢 × ℝ))
32	16, 31	syl 17	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ran 𝐼 → (^◡(1^st ↾ (ℝ × ℝ)) “ 𝑢) = (𝑢 × ℝ))
33		ovex 7189	. . . . . . . . . . . . . 14 ⊢ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ∈ V
34	2, 33	elrnmpo 7287	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ran 𝐼 ↔ ∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
35		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
36	35	xpeq1d 5584	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (𝑢 × ℝ) = (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ))
37		difxp1 6022	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞)) × ℝ) = ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∖ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ))
38		simpl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ∈ ℤ)
39	38	zred 12088	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ∈ ℝ)
40		2rp 12395	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℝ⁺
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 2 ∈ ℝ⁺)
42		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
43	41, 42	rpexpcld 13609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2↑𝑛) ∈ ℝ⁺)
44	39, 43	rerpdivcld 12463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ∈ ℝ)
45	44	rexrd 10691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ∈ ℝ^*)
46		1red 10642	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 1 ∈ ℝ)
47	39, 46	readdcld 10670	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 + 1) ∈ ℝ)
48	47, 43	rerpdivcld 12463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ)
49	48	rexrd 10691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ^*)
50		pnfxr 10695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ +∞ ∈ ℝ^*
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → +∞ ∈ ℝ^*)
52	39	lep1d 11571	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ≤ (𝑥 + 1))
53	39, 47, 43, 52	lediv1dd 12490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ≤ ((𝑥 + 1) / (2↑𝑛)))
54		pnfge 12526	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 + 1) / (2↑𝑛)) ∈ ℝ^* → ((𝑥 + 1) / (2↑𝑛)) ≤ +∞)
55	49, 54	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ≤ +∞)
56		difico 30506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑥 / (2↑𝑛)) ∈ ℝ^* ∧ ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ ((𝑥 / (2↑𝑛)) ≤ ((𝑥 + 1) / (2↑𝑛)) ∧ ((𝑥 + 1) / (2↑𝑛)) ≤ +∞)) → (((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
57	45, 49, 51, 53, 55, 56	syl32anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
58	57	xpeq1d 5584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞)) × ℝ) = (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ))
59	37, 58	syl5reqr 2871	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ) = ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∖ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)))
60	29	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra)
61		ssun1 4148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ⊆ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))
62		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) = (((𝑥 / (2↑𝑛))[,)+∞) × ℝ)
63		oveq1 7163	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑒 = (𝑥 / (2↑𝑛)) → (𝑒[,)+∞) = ((𝑥 / (2↑𝑛))[,)+∞))
64	63	xpeq1d 5584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = (𝑥 / (2↑𝑛)) → ((𝑒[,)+∞) × ℝ) = (((𝑥 / (2↑𝑛))[,)+∞) × ℝ))
65	64	rspceeqv 3638	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 / (2↑𝑛)) ∈ ℝ ∧ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) = (((𝑥 / (2↑𝑛))[,)+∞) × ℝ)) → ∃𝑒 ∈ ℝ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) = ((𝑒[,)+∞) × ℝ))
66	44, 62, 65	sylancl 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ∃𝑒 ∈ ℝ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) = ((𝑒[,)+∞) × ℝ))
67		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) = (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ))
68		ovex 7189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒[,)+∞) ∈ V
69	68, 21	xpex 7476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑒[,)+∞) × ℝ) ∈ V
70	67, 69	elrnmpti 5832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ↔ ∃𝑒 ∈ ℝ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) = ((𝑒[,)+∞) × ℝ))
71	66, 70	sylibr 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)))
72	61, 71	sseldi 3965	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))
73		elsigagen 31406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V ∧ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) → (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
74	26, 72, 73	sylancr 589	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
75		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) = ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)
76		oveq1 7163	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑒 = ((𝑥 + 1) / (2↑𝑛)) → (𝑒[,)+∞) = (((𝑥 + 1) / (2↑𝑛))[,)+∞))
77	76	xpeq1d 5584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = ((𝑥 + 1) / (2↑𝑛)) → ((𝑒[,)+∞) × ℝ) = ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ))
78	77	rspceeqv 3638	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑥 + 1) / (2↑𝑛)) ∈ ℝ ∧ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) = ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)) → ∃𝑒 ∈ ℝ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) = ((𝑒[,)+∞) × ℝ))
79	48, 75, 78	sylancl 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ∃𝑒 ∈ ℝ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) = ((𝑒[,)+∞) × ℝ))
80	67, 69	elrnmpti 5832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ↔ ∃𝑒 ∈ ℝ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) = ((𝑒[,)+∞) × ℝ))
81	79, 80	sylibr 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) ∈ ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)))
82	61, 81	sseldi 3965	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))
83		elsigagen 31406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V ∧ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) → ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
84	26, 82, 83	sylancr 589	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
85		difelsiga 31392	. . . . . . . . . . . . . . . . . . 19 ⊢ (((sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra ∧ (((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∧ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))) → ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∖ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
86	60, 74, 84, 85	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((((𝑥 / (2↑𝑛))[,)+∞) × ℝ) ∖ ((((𝑥 + 1) / (2↑𝑛))[,)+∞) × ℝ)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
87	59, 86	eqeltrd 2913	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
88	87	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
89	36, 88	eqeltrd 2913	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (𝑢 × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
90	89	ex 415	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → (𝑢 × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))))
91	90	rexlimivv 3292	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑢 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → (𝑢 × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
92	34, 91	sylbi 219	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ran 𝐼 → (𝑢 × ℝ) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
93	32, 92	eqeltrd 2913	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ran 𝐼 → (^◡(1^st ↾ (ℝ × ℝ)) “ 𝑢) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
94	93	adantr 483	. . . . . . . . . 10 ⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (^◡(1^st ↾ (ℝ × ℝ)) “ 𝑢) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
95		2ndpreima 30443	. . . . . . . . . . . . 13 ⊢ (𝑣 ⊆ ℝ → (^◡(2^nd ↾ (ℝ × ℝ)) “ 𝑣) = (ℝ × 𝑣))
96	18, 95	syl 17	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ran 𝐼 → (^◡(2^nd ↾ (ℝ × ℝ)) “ 𝑣) = (ℝ × 𝑣))
97	2, 33	elrnmpo 7287	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ran 𝐼 ↔ ∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
98		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
99	98	xpeq2d 5585	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (ℝ × 𝑣) = (ℝ × ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))))
100		difxp2 6023	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℝ × (((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞))) = ((ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∖ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)))
101	57	xpeq2d 5585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ × (((𝑥 / (2↑𝑛))[,)+∞) ∖ (((𝑥 + 1) / (2↑𝑛))[,)+∞))) = (ℝ × ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))))
102	100, 101	syl5reqr 2871	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ × ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) = ((ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∖ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞))))
103		ssun2 4149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))) ⊆ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))
104		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ × ((𝑥 / (2↑𝑛))[,)+∞))
105		oveq1 7163	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = (𝑥 / (2↑𝑛)) → (𝑓[,)+∞) = ((𝑥 / (2↑𝑛))[,)+∞))
106	105	xpeq2d 5585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = (𝑥 / (2↑𝑛)) → (ℝ × (𝑓[,)+∞)) = (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)))
107	106	rspceeqv 3638	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 / (2↑𝑛)) ∈ ℝ ∧ (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ × ((𝑥 / (2↑𝑛))[,)+∞))) → ∃𝑓 ∈ ℝ (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ × (𝑓[,)+∞)))
108	44, 104, 107	sylancl 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ∃𝑓 ∈ ℝ (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ × (𝑓[,)+∞)))
109		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))) = (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))
110		ovex 7189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓[,)+∞) ∈ V
111	21, 110	xpex 7476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℝ × (𝑓[,)+∞)) ∈ V
112	109, 111	elrnmpti 5832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∈ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))) ↔ ∃𝑓 ∈ ℝ (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) = (ℝ × (𝑓[,)+∞)))
113	108, 112	sylibr 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∈ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))
114	103, 113	sseldi 3965	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))
115		elsigagen 31406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V ∧ (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) → (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
116	26, 114, 115	sylancr 589	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
117		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞))
118		oveq1 7163	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ((𝑥 + 1) / (2↑𝑛)) → (𝑓[,)+∞) = (((𝑥 + 1) / (2↑𝑛))[,)+∞))
119	118	xpeq2d 5585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ((𝑥 + 1) / (2↑𝑛)) → (ℝ × (𝑓[,)+∞)) = (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)))
120	119	rspceeqv 3638	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑥 + 1) / (2↑𝑛)) ∈ ℝ ∧ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞))) → ∃𝑓 ∈ ℝ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = (ℝ × (𝑓[,)+∞)))
121	48, 117, 120	sylancl 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ∃𝑓 ∈ ℝ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = (ℝ × (𝑓[,)+∞)))
122	109, 111	elrnmpti 5832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) ∈ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))) ↔ ∃𝑓 ∈ ℝ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) = (ℝ × (𝑓[,)+∞)))
123	121, 122	sylibr 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) ∈ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))
124	103, 123	sseldi 3965	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))
125		elsigagen 31406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V ∧ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) ∈ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) → (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
126	26, 124, 125	sylancr 589	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
127		difelsiga 31392	. . . . . . . . . . . . . . . . . . 19 ⊢ (((sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra ∧ (ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∧ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))) → ((ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∖ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞))) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
128	60, 116, 126, 127	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((ℝ × ((𝑥 / (2↑𝑛))[,)+∞)) ∖ (ℝ × (((𝑥 + 1) / (2↑𝑛))[,)+∞))) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
129	102, 128	eqeltrd 2913	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (ℝ × ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
130	129	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (ℝ × ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
131	99, 130	eqeltrd 2913	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (ℝ × 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
132	131	ex 415	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → (ℝ × 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))))
133	132	rexlimivv 3292	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑣 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → (ℝ × 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
134	97, 133	sylbi 219	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ ran 𝐼 → (ℝ × 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
135	96, 134	eqeltrd 2913	. . . . . . . . . . 11 ⊢ (𝑣 ∈ ran 𝐼 → (^◡(2^nd ↾ (ℝ × ℝ)) “ 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
136	135	adantl 484	. . . . . . . . . 10 ⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (^◡(2^nd ↾ (ℝ × ℝ)) “ 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
137		inelsiga 31394	. . . . . . . . . 10 ⊢ (((sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∈ ∪ ran sigAlgebra ∧ (^◡(1^st ↾ (ℝ × ℝ)) “ 𝑢) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∧ (^◡(2^nd ↾ (ℝ × ℝ)) “ 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))) → ((^◡(1^st ↾ (ℝ × ℝ)) “ 𝑢) ∩ (^◡(2^nd ↾ (ℝ × ℝ)) “ 𝑣)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
138	30, 94, 136, 137	syl3anc 1367	. . . . . . . . 9 ⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → ((^◡(1^st ↾ (ℝ × ℝ)) “ 𝑢) ∩ (^◡(2^nd ↾ (ℝ × ℝ)) “ 𝑣)) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
139	20, 138	eqeltrd 2913	. . . . . . . 8 ⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (𝑢 × 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
140	139	adantr 483	. . . . . . 7 ⊢ (((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) ∧ 𝑑 = (𝑢 × 𝑣)) → (𝑢 × 𝑣) ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
141	11, 140	eqeltrd 2913	. . . . . 6 ⊢ (((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) ∧ 𝑑 = (𝑢 × 𝑣)) → 𝑑 ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
142	141	ex 415	. . . . 5 ⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (𝑑 = (𝑢 × 𝑣) → 𝑑 ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))))
143	142	rexlimivv 3292	. . . 4 ⊢ (∃𝑢 ∈ ran 𝐼∃𝑣 ∈ ran 𝐼 𝑑 = (𝑢 × 𝑣) → 𝑑 ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
144	10, 143	sylbi 219	. . 3 ⊢ (𝑑 ∈ ran 𝑅 → 𝑑 ∈ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
145	144	ssriv 3971	. 2 ⊢ ran 𝑅 ⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))
146		sigagenss2 31409	. 2 ⊢ ((∪ ran 𝑅 = ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∧ ran 𝑅 ⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ∧ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) ∈ V) → (sigaGen‘ran 𝑅) ⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))))
147	6, 145, 26, 146	mp3an 1457	1 ⊢ (sigaGen‘ran 𝑅) ⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))

Colors of variables: wff setvar class

Syntax hints: ∧ wa 398 = wceq 1537 ⊤wtru 1538 ∈ wcel 2114 ∃wrex 3139 Vcvv 3494 ∖ cdif 3933 ∪ cun 3934 ∩ cin 3935 ⊆ wss 3936 𝒫 cpw 4539 ∪ cuni 4838 class class class wbr 5066 ↦ cmpt 5146 × cxp 5553 ^◡ccnv 5554 ran crn 5556 ↾ cres 5557 “ cima 5558 ‘cfv 6355 (class class class)co 7156 ∈ cmpo 7158 1^st c1st 7687 2^nd c2nd 7688 ℝcr 10536 1c1 10538 + caddc 10540 +∞cpnf 10672 ℝ^*cxr 10674 ≤ cle 10676 / cdiv 11297 2c2 11693 ℤcz 11982 ℝ⁺crp 12390 (,)cioo 12739 [,)cico 12741 ↑cexp 13430 topGenctg 16711 sigAlgebracsiga 31367 sigaGencsigagen 31397 𝔅_ℝcbrsiga 31440

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-inf2 9104 ax-ac2 9885 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615 ax-addf 10616 ax-mulf 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-om 7581 df-1st 7689 df-2nd 7690 df-supp 7831 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-2o 8103 df-oadd 8106 df-er 8289 df-map 8408 df-pm 8409 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fsupp 8834 df-fi 8875 df-sup 8906 df-inf 8907 df-oi 8974 df-dju 9330 df-card 9368 df-acn 9371 df-ac 9542 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-z 11983 df-dec 12100 df-uz 12245 df-q 12350 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ioo 12743 df-ioc 12744 df-ico 12745 df-icc 12746 df-fz 12894 df-fzo 13035 df-fl 13163 df-mod 13239 df-seq 13371 df-exp 13431 df-fac 13635 df-bc 13664 df-hash 13692 df-shft 14426 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-limsup 14828 df-clim 14845 df-rlim 14846 df-sum 15043 df-ef 15421 df-sin 15423 df-cos 15424 df-pi 15426 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-mulr 16579 df-starv 16580 df-sca 16581 df-vsca 16582 df-ip 16583 df-tset 16584 df-ple 16585 df-ds 16587 df-unif 16588 df-hom 16589 df-cco 16590 df-rest 16696 df-topn 16697 df-0g 16715 df-gsum 16716 df-topgen 16717 df-pt 16718 df-prds 16721 df-xrs 16775 df-qtop 16780 df-imas 16781 df-xps 16783 df-mre 16857 df-mrc 16858 df-acs 16860 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-submnd 17957 df-mulg 18225 df-cntz 18447 df-cmn 18908 df-psmet 20537 df-xmet 20538 df-met 20539 df-bl 20540 df-mopn 20541 df-fbas 20542 df-fg 20543 df-cnfld 20546 df-refld 20749 df-top 21502 df-topon 21519 df-topsp 21541 df-bases 21554 df-cld 21627 df-ntr 21628 df-cls 21629 df-nei 21706 df-lp 21744 df-perf 21745 df-cn 21835 df-cnp 21836 df-haus 21923 df-cmp 21995 df-tx 22170 df-hmeo 22363 df-fil 22454 df-fm 22546 df-flim 22547 df-flf 22548 df-fcls 22549 df-xms 22930 df-ms 22931 df-tms 22932 df-cncf 23486 df-cfil 23858 df-cmet 23860 df-cms 23938 df-limc 24464 df-dv 24465 df-log 25140 df-cxp 25141 df-logb 25343 df-siga 31368 df-sigagen 31398 df-brsiga 31441

This theorem is referenced by: sxbrsigalem4 31545

W3C validator