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	$⊢ 𝔅_{ℝ} \times_{s} 𝔅_{ℝ} = 𝛔 (J \times_{t} J)$

Proof

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

Metamath Proof Explorer

Theorem sxbrsiga

Proof