Metamath Proof Explorer

Theorem 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 ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) = ( ℝ × ℝ )

Proof

Step Hyp Ref Expression
1 brsigasspwrn ⊢ 𝔅ℝ ⊆ 𝒫 ℝ
2 1 sseli ⊢ ( 𝑥 ∈ 𝔅ℝ → 𝑥 ∈ 𝒫 ℝ )
3 2 elpwid ⊢ ( 𝑥 ∈ 𝔅ℝ → 𝑥 ⊆ ℝ )
4 1 sseli ⊢ ( 𝑦 ∈ 𝔅ℝ → 𝑦 ∈ 𝒫 ℝ )
5 4 elpwid ⊢ ( 𝑦 ∈ 𝔅ℝ → 𝑦 ⊆ ℝ )
6 xpss12 ⊢ ( ( 𝑥 ⊆ ℝ ∧ 𝑦 ⊆ ℝ ) → ( 𝑥 × 𝑦 ) ⊆ ( ℝ × ℝ ) )
7 3 5 6 syl2an ⊢ ( ( 𝑥 ∈ 𝔅ℝ ∧ 𝑦 ∈ 𝔅ℝ ) → ( 𝑥 × 𝑦 ) ⊆ ( ℝ × ℝ ) )
8 vex ⊢ 𝑥 ∈ V
9 vex ⊢ 𝑦 ∈ V
10 8 9 xpex ⊢ ( 𝑥 × 𝑦 ) ∈ V
11 10 elpw ⊢ ( ( 𝑥 × 𝑦 ) ∈ 𝒫 ( ℝ × ℝ ) ↔ ( 𝑥 × 𝑦 ) ⊆ ( ℝ × ℝ ) )
12 7 11 sylibr ⊢ ( ( 𝑥 ∈ 𝔅ℝ ∧ 𝑦 ∈ 𝔅ℝ ) → ( 𝑥 × 𝑦 ) ∈ 𝒫 ( ℝ × ℝ ) )
13 12 rgen2 ⊢ ∀ 𝑥 ∈ 𝔅ℝ ∀ 𝑦 ∈ 𝔅ℝ ( 𝑥 × 𝑦 ) ∈ 𝒫 ( ℝ × ℝ )
14 eqid ⊢ ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) )
15 14 rnmposs ⊢ ( ∀ 𝑥 ∈ 𝔅ℝ ∀ 𝑦 ∈ 𝔅ℝ ( 𝑥 × 𝑦 ) ∈ 𝒫 ( ℝ × ℝ ) → ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) ⊆ 𝒫 ( ℝ × ℝ ) )
16 13 15 ax-mp ⊢ ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) ⊆ 𝒫 ( ℝ × ℝ )
17 unibrsiga ⊢ ∪ 𝔅ℝ = ℝ
18 brsigarn ⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ )
19 elrnsiga ⊢ ( 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) → 𝔅ℝ ∈ ∪ ran sigAlgebra )
20 unielsiga ⊢ ( 𝔅ℝ ∈ ∪ ran sigAlgebra → ∪ 𝔅ℝ ∈ 𝔅ℝ )
21 18 19 20 mp2b ⊢ ∪ 𝔅ℝ ∈ 𝔅ℝ
22 17 21 eqeltrri ⊢ ℝ ∈ 𝔅ℝ
23 eqid ⊢ ( ℝ × ℝ ) = ( ℝ × ℝ )
24 xpeq1 ⊢ ( 𝑥 = ℝ → ( 𝑥 × 𝑦 ) = ( ℝ × 𝑦 ) )
25 24 eqeq2d ⊢ ( 𝑥 = ℝ → ( ( ℝ × ℝ ) = ( 𝑥 × 𝑦 ) ↔ ( ℝ × ℝ ) = ( ℝ × 𝑦 ) ) )
26 xpeq2 ⊢ ( 𝑦 = ℝ → ( ℝ × 𝑦 ) = ( ℝ × ℝ ) )
27 26 eqeq2d ⊢ ( 𝑦 = ℝ → ( ( ℝ × ℝ ) = ( ℝ × 𝑦 ) ↔ ( ℝ × ℝ ) = ( ℝ × ℝ ) ) )
28 25 27 rspc2ev ⊢ ( ( ℝ ∈ 𝔅ℝ ∧ ℝ ∈ 𝔅ℝ ∧ ( ℝ × ℝ ) = ( ℝ × ℝ ) ) → ∃ 𝑥 ∈ 𝔅ℝ ∃ 𝑦 ∈ 𝔅ℝ ( ℝ × ℝ ) = ( 𝑥 × 𝑦 ) )
29 22 22 23 28 mp3an ⊢ ∃ 𝑥 ∈ 𝔅ℝ ∃ 𝑦 ∈ 𝔅ℝ ( ℝ × ℝ ) = ( 𝑥 × 𝑦 )
30 14 10 elrnmpo ⊢ ( ( ℝ × ℝ ) ∈ ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝔅ℝ ∃ 𝑦 ∈ 𝔅ℝ ( ℝ × ℝ ) = ( 𝑥 × 𝑦 ) )
31 29 30 mpbir ⊢ ( ℝ × ℝ ) ∈ ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) )
32 elpwuni ⊢ ( ( ℝ × ℝ ) ∈ ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) → ( ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) ⊆ 𝒫 ( ℝ × ℝ ) ↔ ∪ ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) = ( ℝ × ℝ ) ) )
33 31 32 ax-mp ⊢ ( ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) ⊆ 𝒫 ( ℝ × ℝ ) ↔ ∪ ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) = ( ℝ × ℝ ) )
34 16 33 mpbi ⊢ ∪ ran ( 𝑥 ∈ 𝔅ℝ , 𝑦 ∈ 𝔅ℝ ↦ ( 𝑥 × 𝑦 ) ) = ( ℝ × ℝ )