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 𝑅 )