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	⊢ 𝐽 = ( topGen ‘ ran (,) )
Assertion	sxbrsiga	⊢ ( 𝔅ℝ ×s 𝔅ℝ ) = ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) )

Proof

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