br2base

Description: The base set for the generator of the Borel sigma-algebra on ( RR X. RR ) is indeed ( RR X. RR ) . (Contributed by Thierry Arnoux, 22-Sep-2017)

		Ref	Expression
	Assertion	br2base	$⊢ ⋃ ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) = ℝ^{2}$

Proof

Step	Hyp	Ref	Expression
1		brsigasspwrn	$⊢ 𝔅_{ℝ} \subseteq 𝒫 ℝ$
2	1	sseli	$⊢ x \in 𝔅_{ℝ} \to x \in 𝒫 ℝ$
3	2	elpwid	$⊢ x \in 𝔅_{ℝ} \to x \subseteq ℝ$
4	1	sseli	$⊢ y \in 𝔅_{ℝ} \to y \in 𝒫 ℝ$
5	4	elpwid	$⊢ y \in 𝔅_{ℝ} \to y \subseteq ℝ$
6		xpss12	$⊢ (x \subseteq ℝ \land y \subseteq ℝ) \to x \times y \subseteq ℝ^{2}$
7	3 5 6	syl2an	$⊢ (x \in 𝔅_{ℝ} \land y \in 𝔅_{ℝ}) \to x \times y \subseteq ℝ^{2}$
8		vex	$⊢ x \in V$
9		vex	$⊢ y \in V$
10	8 9	xpex	$⊢ x \times y \in V$
11	10	elpw	$⊢ x \times y \in 𝒫 ℝ^{2} \leftrightarrow x \times y \subseteq ℝ^{2}$
12	7 11	sylibr	$⊢ (x \in 𝔅_{ℝ} \land y \in 𝔅_{ℝ}) \to x \times y \in 𝒫 ℝ^{2}$
13	12	rgen2	$⊢ \forall x \in 𝔅_{ℝ} \forall y \in 𝔅_{ℝ} x \times y \in 𝒫 ℝ^{2}$
14		eqid	$⊢ (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) = (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y)$
15	14	rnmposs	$⊢ \forall x \in 𝔅_{ℝ} \forall y \in 𝔅_{ℝ} x \times y \in 𝒫 ℝ^{2} \to ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) \subseteq 𝒫 ℝ^{2}$
16	13 15	ax-mp	$⊢ ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) \subseteq 𝒫 ℝ^{2}$
17		unibrsiga	$⊢ ⋃ 𝔅_{ℝ} = ℝ$
18		brsigarn	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ)$
19		elrnsiga	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ) \to 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
20		unielsiga	$⊢ 𝔅_{ℝ} \in ⋃ ran sigAlgebra \to ⋃ 𝔅_{ℝ} \in 𝔅_{ℝ}$
21	18 19 20	mp2b	$⊢ ⋃ 𝔅_{ℝ} \in 𝔅_{ℝ}$
22	17 21	eqeltrri	$⊢ ℝ \in 𝔅_{ℝ}$
23		eqid	$⊢ ℝ^{2} = ℝ^{2}$
24		xpeq1	$⊢ x = ℝ \to x \times y = ℝ \times y$
25	24	eqeq2d	$⊢ x = ℝ \to (ℝ^{2} = x \times y \leftrightarrow ℝ^{2} = ℝ \times y)$
26		xpeq2	$⊢ y = ℝ \to ℝ \times y = ℝ^{2}$
27	26	eqeq2d	$⊢ y = ℝ \to (ℝ^{2} = ℝ \times y \leftrightarrow ℝ^{2} = ℝ^{2})$
28	25 27	rspc2ev	$⊢ (ℝ \in 𝔅_{ℝ} \land ℝ \in 𝔅_{ℝ} \land ℝ^{2} = ℝ^{2}) \to \exists x \in 𝔅_{ℝ} \exists y \in 𝔅_{ℝ} ℝ^{2} = x \times y$
29	22 22 23 28	mp3an	$⊢ \exists x \in 𝔅_{ℝ} \exists y \in 𝔅_{ℝ} ℝ^{2} = x \times y$
30	14 10	elrnmpo	$⊢ ℝ^{2} \in ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) \leftrightarrow \exists x \in 𝔅_{ℝ} \exists y \in 𝔅_{ℝ} ℝ^{2} = x \times y$
31	29 30	mpbir	$⊢ ℝ^{2} \in ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y)$
32		elpwuni	$⊢ ℝ^{2} \in ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) \to (ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) \subseteq 𝒫 ℝ^{2} \leftrightarrow ⋃ ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) = ℝ^{2})$
33	31 32	ax-mp	$⊢ ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) \subseteq 𝒫 ℝ^{2} \leftrightarrow ⋃ ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) = ℝ^{2}$
34	16 33	mpbi	$⊢ ⋃ ran (x \in 𝔅_{ℝ}, y \in 𝔅_{ℝ} ⟼ x \times y) = ℝ^{2}$

Metamath Proof Explorer

Theorem br2base

Proof