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 ⊢ 𝐽 = ( topGen ‘ ran (,) )
dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
dya2ioc.2 ⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
Assertion sxbrsigalem1 ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ran 𝑅 )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 dya2ioc.2 ⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
4 1 2 3 dya2iocucvr ⊢ ∪ ran 𝑅 = ( ℝ × ℝ )
5 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
6 1 5 eqeltri ⊢ 𝐽 ∈ Top
7 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
8 1 unieqi ⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
9 7 8 eqtr4i ⊢ ℝ = ∪ 𝐽
10 6 6 9 9 txunii ⊢ ( ℝ × ℝ ) = ∪ ( 𝐽 ×t 𝐽 )
11 4 10 eqtr2i ⊢ ∪ ( 𝐽 ×t 𝐽 ) = ∪ ran 𝑅
12 1 2 3 dya2iocuni ⊢ ( 𝑥 ∈ ( 𝐽 ×t 𝐽 ) → ∃ 𝑦 ∈ 𝒫 ran 𝑅 ∪ 𝑦 = 𝑥 )
13 simpr ⊢ ( ( 𝑦 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑦 = 𝑥 ) → ∪ 𝑦 = 𝑥 )
14 1 2 3 dya2iocct ⊢ ran 𝑅 ≼ ω
15 ctex ⊢ ( ran 𝑅 ≼ ω → ran 𝑅 ∈ V )
16 14 15 mp1i ⊢ ( 𝑦 ∈ 𝒫 ran 𝑅 → ran 𝑅 ∈ V )
17 elpwi ⊢ ( 𝑦 ∈ 𝒫 ran 𝑅 → 𝑦 ⊆ ran 𝑅 )
18 ssct ⊢ ( ( 𝑦 ⊆ ran 𝑅 ∧ ran 𝑅 ≼ ω ) → 𝑦 ≼ ω )
19 17 14 18 sylancl ⊢ ( 𝑦 ∈ 𝒫 ran 𝑅 → 𝑦 ≼ ω )
20 elsigagen2 ⊢ ( ( ran 𝑅 ∈ V ∧ 𝑦 ⊆ ran 𝑅 ∧ 𝑦 ≼ ω ) → ∪ 𝑦 ∈ ( sigaGen ‘ ran 𝑅 ) )
21 16 17 19 20 syl3anc ⊢ ( 𝑦 ∈ 𝒫 ran 𝑅 → ∪ 𝑦 ∈ ( sigaGen ‘ ran 𝑅 ) )
22 21 adantr ⊢ ( ( 𝑦 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑦 = 𝑥 ) → ∪ 𝑦 ∈ ( sigaGen ‘ ran 𝑅 ) )
23 13 22 eqeltrrd ⊢ ( ( 𝑦 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑦 = 𝑥 ) → 𝑥 ∈ ( sigaGen ‘ ran 𝑅 ) )
24 23 rexlimiva ⊢ ( ∃ 𝑦 ∈ 𝒫 ran 𝑅 ∪ 𝑦 = 𝑥 → 𝑥 ∈ ( sigaGen ‘ ran 𝑅 ) )
25 12 24 syl ⊢ ( 𝑥 ∈ ( 𝐽 ×t 𝐽 ) → 𝑥 ∈ ( sigaGen ‘ ran 𝑅 ) )
26 25 ssriv ⊢ ( 𝐽 ×t 𝐽 ) ⊆ ( sigaGen ‘ ran 𝑅 )
27 14 15 ax-mp ⊢ ran 𝑅 ∈ V
28 sigagenss2 ⊢ ( ( ∪ ( 𝐽 ×t 𝐽 ) = ∪ ran 𝑅 ∧ ( 𝐽 ×t 𝐽 ) ⊆ ( sigaGen ‘ ran 𝑅 ) ∧ ran 𝑅 ∈ V ) → ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ran 𝑅 ) )
29 11 26 27 28 mp3an ⊢ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ran 𝑅 )