Metamath Proof Explorer

Theorem 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 ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n
dya2ioc.2 ⊢ R = u ∈ ran ⁡ I , v ∈ ran ⁡ I ⟼ u × v
Assertion sxbrsigalem1 ⊢ 𝛔 ⁡ J × t J ⊆ 𝛔 ⁡ ran ⁡ R

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
2 dya2ioc.1 ⊢ I = x ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n
3 dya2ioc.2 ⊢ R = u ∈ ran ⁡ I , v ∈ ran ⁡ I ⟼ u × v
4 1 2 3 dya2iocucvr ⊢ ⋃ ran ⁡ R = ℝ 2
5 retop ⊢ topGen ⁡ ran ⁡ . ∈ Top
6 1 5 eqeltri ⊢ J ∈ Top
7 uniretop ⊢ ℝ = ⋃ topGen ⁡ ran ⁡ .
8 1 unieqi ⊢ ⋃ J = ⋃ topGen ⁡ ran ⁡ .
9 7 8 eqtr4i ⊢ ℝ = ⋃ J
10 6 6 9 9 txunii ⊢ ℝ 2 = ⋃ J × t J
11 4 10 eqtr2i ⊢ ⋃ J × t J = ⋃ ran ⁡ R
12 1 2 3 dya2iocuni ⊢ x ∈ J × t J → ∃ y ∈ 𝒫 ran ⁡ R ⋃ y = x
13 simpr ⊢ y ∈ 𝒫 ran ⁡ R ∧ ⋃ y = x → ⋃ y = x
14 1 2 3 dya2iocct ⊢ ran ⁡ R ≼ ω
15 ctex ⊢ ran ⁡ R ≼ ω → ran ⁡ R ∈ V
16 14 15 mp1i ⊢ y ∈ 𝒫 ran ⁡ R → ran ⁡ R ∈ V
17 elpwi ⊢ y ∈ 𝒫 ran ⁡ R → y ⊆ ran ⁡ R
18 ssct ⊢ y ⊆ ran ⁡ R ∧ ran ⁡ R ≼ ω → y ≼ ω
19 17 14 18 sylancl ⊢ y ∈ 𝒫 ran ⁡ R → y ≼ ω
20 elsigagen2 ⊢ ran ⁡ R ∈ V ∧ y ⊆ ran ⁡ R ∧ y ≼ ω → ⋃ y ∈ 𝛔 ⁡ ran ⁡ R
21 16 17 19 20 syl3anc ⊢ y ∈ 𝒫 ran ⁡ R → ⋃ y ∈ 𝛔 ⁡ ran ⁡ R
22 21 adantr ⊢ y ∈ 𝒫 ran ⁡ R ∧ ⋃ y = x → ⋃ y ∈ 𝛔 ⁡ ran ⁡ R
23 13 22 eqeltrrd ⊢ y ∈ 𝒫 ran ⁡ R ∧ ⋃ y = x → x ∈ 𝛔 ⁡ ran ⁡ R
24 23 rexlimiva ⊢ ∃ y ∈ 𝒫 ran ⁡ R ⋃ y = x → x ∈ 𝛔 ⁡ ran ⁡ R
25 12 24 syl ⊢ x ∈ J × t J → x ∈ 𝛔 ⁡ ran ⁡ R
26 25 ssriv ⊢ J × t J ⊆ 𝛔 ⁡ ran ⁡ R
27 14 15 ax-mp ⊢ ran ⁡ R ∈ V
28 sigagenss2 ⊢ ⋃ J × t J = ⋃ ran ⁡ R ∧ J × t J ⊆ 𝛔 ⁡ ran ⁡ R ∧ ran ⁡ R ∈ V → 𝛔 ⁡ J × t J ⊆ 𝛔 ⁡ ran ⁡ R
29 11 26 27 28 mp3an ⊢ 𝛔 ⁡ J × t J ⊆ 𝛔 ⁡ ran ⁡ R