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