Metamath Proof Explorer

Theorem sxbrsiga

Description: The product sigma-algebra ( BrSiga sX BrSiga ) is the Borel algebra on ( RR X. RR ) See example 5.1.1 of Cohn p. 143 . (Contributed by Thierry Arnoux, 10-Oct-2017)

Ref Expression
Hypothesis sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
Assertion sxbrsiga ⊢ 𝔅 ℝ × s 𝔅 ℝ = 𝛔 ⁡ J × t J

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
2 brsigarn ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ
3 eqid ⊢ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f = ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f
4 3 sxval ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ ∧ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ → 𝔅 ℝ × s 𝔅 ℝ = 𝛔 ⁡ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f
5 2 2 4 mp2an ⊢ 𝔅 ℝ × s 𝔅 ℝ = 𝛔 ⁡ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f
6 br2base ⊢ ⋃ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f = ℝ 2
7 1 tpr2uni ⊢ ⋃ J × t J = ℝ 2
8 6 7 eqtr4i ⊢ ⋃ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f = ⋃ J × t J
9 brsigasspwrn ⊢ 𝔅 ℝ ⊆ 𝒫 ℝ
10 9 sseli ⊢ e ∈ 𝔅 ℝ → e ∈ 𝒫 ℝ
11 10 elpwid ⊢ e ∈ 𝔅 ℝ → e ⊆ ℝ
12 9 sseli ⊢ f ∈ 𝔅 ℝ → f ∈ 𝒫 ℝ
13 12 elpwid ⊢ f ∈ 𝔅 ℝ → f ⊆ ℝ
14 xpinpreima2 ⊢ e ⊆ ℝ ∧ f ⊆ ℝ → e × f = 1 st ↾ ℝ 2 -1 e ∩ 2 nd ↾ ℝ 2 -1 f
15 11 13 14 syl2an ⊢ e ∈ 𝔅 ℝ ∧ f ∈ 𝔅 ℝ → e × f = 1 st ↾ ℝ 2 -1 e ∩ 2 nd ↾ ℝ 2 -1 f
16 1 tpr2tp ⊢ J × t J ∈ TopOn ⁡ ℝ 2
17 sigagensiga ⊢ J × t J ∈ TopOn ⁡ ℝ 2 → 𝛔 ⁡ J × t J ∈ sigAlgebra ⁡ ⋃ J × t J
18 16 17 ax-mp ⊢ 𝛔 ⁡ J × t J ∈ sigAlgebra ⁡ ⋃ J × t J
19 elrnsiga ⊢ 𝛔 ⁡ J × t J ∈ sigAlgebra ⁡ ⋃ J × t J → 𝛔 ⁡ J × t J ∈ ⋃ ran ⁡ sigAlgebra
20 18 19 mp1i ⊢ e ∈ 𝔅 ℝ ∧ f ∈ 𝔅 ℝ → 𝛔 ⁡ J × t J ∈ ⋃ ran ⁡ sigAlgebra
21 16 a1i ⊢ e ∈ 𝔅 ℝ → J × t J ∈ TopOn ⁡ ℝ 2
22 21 sgsiga ⊢ e ∈ 𝔅 ℝ → 𝛔 ⁡ J × t J ∈ ⋃ ran ⁡ sigAlgebra
23 elrnsiga ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
24 2 23 mp1i ⊢ e ∈ 𝔅 ℝ → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
25 retopon ⊢ topGen ⁡ ran ⁡ . ∈ TopOn ⁡ ℝ
26 1 25 eqeltri ⊢ J ∈ TopOn ⁡ ℝ
27 tx1cn ⊢ J ∈ TopOn ⁡ ℝ ∧ J ∈ TopOn ⁡ ℝ → 1 st ↾ ℝ 2 ∈ J × t J Cn J
28 26 26 27 mp2an ⊢ 1 st ↾ ℝ 2 ∈ J × t J Cn J
29 28 a1i ⊢ e ∈ 𝔅 ℝ → 1 st ↾ ℝ 2 ∈ J × t J Cn J
30 eqidd ⊢ e ∈ 𝔅 ℝ → 𝛔 ⁡ J × t J = 𝛔 ⁡ J × t J
31 df-brsiga ⊢ 𝔅 ℝ = 𝛔 ⁡ topGen ⁡ ran ⁡ .
32 1 fveq2i ⊢ 𝛔 ⁡ J = 𝛔 ⁡ topGen ⁡ ran ⁡ .
33 31 32 eqtr4i ⊢ 𝔅 ℝ = 𝛔 ⁡ J
34 33 a1i ⊢ e ∈ 𝔅 ℝ → 𝔅 ℝ = 𝛔 ⁡ J
35 29 30 34 cnmbfm ⊢ e ∈ 𝔅 ℝ → 1 st ↾ ℝ 2 ∈ 𝛔 ⁡ J × t J MblFn μ 𝔅 ℝ
36 id ⊢ e ∈ 𝔅 ℝ → e ∈ 𝔅 ℝ
37 22 24 35 36 mbfmcnvima ⊢ e ∈ 𝔅 ℝ → 1 st ↾ ℝ 2 -1 e ∈ 𝛔 ⁡ J × t J
38 37 adantr ⊢ e ∈ 𝔅 ℝ ∧ f ∈ 𝔅 ℝ → 1 st ↾ ℝ 2 -1 e ∈ 𝛔 ⁡ J × t J
39 16 a1i ⊢ f ∈ 𝔅 ℝ → J × t J ∈ TopOn ⁡ ℝ 2
40 39 sgsiga ⊢ f ∈ 𝔅 ℝ → 𝛔 ⁡ J × t J ∈ ⋃ ran ⁡ sigAlgebra
41 2 23 mp1i ⊢ f ∈ 𝔅 ℝ → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
42 tx2cn ⊢ J ∈ TopOn ⁡ ℝ ∧ J ∈ TopOn ⁡ ℝ → 2 nd ↾ ℝ 2 ∈ J × t J Cn J
43 26 26 42 mp2an ⊢ 2 nd ↾ ℝ 2 ∈ J × t J Cn J
44 43 a1i ⊢ f ∈ 𝔅 ℝ → 2 nd ↾ ℝ 2 ∈ J × t J Cn J
45 eqidd ⊢ f ∈ 𝔅 ℝ → 𝛔 ⁡ J × t J = 𝛔 ⁡ J × t J
46 33 a1i ⊢ f ∈ 𝔅 ℝ → 𝔅 ℝ = 𝛔 ⁡ J
47 44 45 46 cnmbfm ⊢ f ∈ 𝔅 ℝ → 2 nd ↾ ℝ 2 ∈ 𝛔 ⁡ J × t J MblFn μ 𝔅 ℝ
48 id ⊢ f ∈ 𝔅 ℝ → f ∈ 𝔅 ℝ
49 40 41 47 48 mbfmcnvima ⊢ f ∈ 𝔅 ℝ → 2 nd ↾ ℝ 2 -1 f ∈ 𝛔 ⁡ J × t J
50 49 adantl ⊢ e ∈ 𝔅 ℝ ∧ f ∈ 𝔅 ℝ → 2 nd ↾ ℝ 2 -1 f ∈ 𝛔 ⁡ J × t J
51 inelsiga ⊢ 𝛔 ⁡ J × t J ∈ ⋃ ran ⁡ sigAlgebra ∧ 1 st ↾ ℝ 2 -1 e ∈ 𝛔 ⁡ J × t J ∧ 2 nd ↾ ℝ 2 -1 f ∈ 𝛔 ⁡ J × t J → 1 st ↾ ℝ 2 -1 e ∩ 2 nd ↾ ℝ 2 -1 f ∈ 𝛔 ⁡ J × t J
52 20 38 50 51 syl3anc ⊢ e ∈ 𝔅 ℝ ∧ f ∈ 𝔅 ℝ → 1 st ↾ ℝ 2 -1 e ∩ 2 nd ↾ ℝ 2 -1 f ∈ 𝛔 ⁡ J × t J
53 15 52 eqeltrd ⊢ e ∈ 𝔅 ℝ ∧ f ∈ 𝔅 ℝ → e × f ∈ 𝛔 ⁡ J × t J
54 53 rgen2 ⊢ ∀ e ∈ 𝔅 ℝ ∀ f ∈ 𝔅 ℝ e × f ∈ 𝛔 ⁡ J × t J
55 eqid ⊢ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f = e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f
56 55 rnmposs ⊢ ∀ e ∈ 𝔅 ℝ ∀ f ∈ 𝔅 ℝ e × f ∈ 𝛔 ⁡ J × t J → ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f ⊆ 𝛔 ⁡ J × t J
57 54 56 ax-mp ⊢ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f ⊆ 𝛔 ⁡ J × t J
58 sigagenss2 ⊢ ⋃ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f = ⋃ J × t J ∧ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f ⊆ 𝛔 ⁡ J × t J ∧ J × t J ∈ TopOn ⁡ ℝ 2 → 𝛔 ⁡ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f ⊆ 𝛔 ⁡ J × t J
59 8 57 16 58 mp3an ⊢ 𝛔 ⁡ ran ⁡ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f ⊆ 𝛔 ⁡ J × t J
60 5 59 eqsstri ⊢ 𝔅 ℝ × s 𝔅 ℝ ⊆ 𝛔 ⁡ J × t J
61 1 sxbrsigalem6 ⊢ 𝛔 ⁡ J × t J ⊆ 𝔅 ℝ × s 𝔅 ℝ
62 60 61 eqssi ⊢ 𝔅 ℝ × s 𝔅 ℝ = 𝛔 ⁡ J × t J