Proof of Theorem br2base
| Step | Hyp | Ref
| Expression |
| 1 | | brsigasspwrn 34186 |
. . . . . . . 8
⊢
𝔅ℝ ⊆ 𝒫 ℝ |
| 2 | 1 | sseli 3979 |
. . . . . . 7
⊢ (𝑥 ∈
𝔅ℝ → 𝑥 ∈ 𝒫 ℝ) |
| 3 | 2 | elpwid 4609 |
. . . . . 6
⊢ (𝑥 ∈
𝔅ℝ → 𝑥 ⊆ ℝ) |
| 4 | 1 | sseli 3979 |
. . . . . . 7
⊢ (𝑦 ∈
𝔅ℝ → 𝑦 ∈ 𝒫 ℝ) |
| 5 | 4 | elpwid 4609 |
. . . . . 6
⊢ (𝑦 ∈
𝔅ℝ → 𝑦 ⊆ ℝ) |
| 6 | | xpss12 5700 |
. . . . . 6
⊢ ((𝑥 ⊆ ℝ ∧ 𝑦 ⊆ ℝ) → (𝑥 × 𝑦) ⊆ (ℝ ×
ℝ)) |
| 7 | 3, 5, 6 | syl2an 596 |
. . . . 5
⊢ ((𝑥 ∈
𝔅ℝ ∧ 𝑦 ∈ 𝔅ℝ) →
(𝑥 × 𝑦) ⊆ (ℝ ×
ℝ)) |
| 8 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 9 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 10 | 8, 9 | xpex 7773 |
. . . . . 6
⊢ (𝑥 × 𝑦) ∈ V |
| 11 | 10 | elpw 4604 |
. . . . 5
⊢ ((𝑥 × 𝑦) ∈ 𝒫 (ℝ × ℝ)
↔ (𝑥 × 𝑦) ⊆ (ℝ ×
ℝ)) |
| 12 | 7, 11 | sylibr 234 |
. . . 4
⊢ ((𝑥 ∈
𝔅ℝ ∧ 𝑦 ∈ 𝔅ℝ) →
(𝑥 × 𝑦) ∈ 𝒫 (ℝ
× ℝ)) |
| 13 | 12 | rgen2 3199 |
. . 3
⊢
∀𝑥 ∈
𝔅ℝ ∀𝑦 ∈ 𝔅ℝ (𝑥 × 𝑦) ∈ 𝒫 (ℝ ×
ℝ) |
| 14 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈
𝔅ℝ, 𝑦 ∈ 𝔅ℝ ↦
(𝑥 × 𝑦)) = (𝑥 ∈ 𝔅ℝ, 𝑦 ∈
𝔅ℝ ↦ (𝑥 × 𝑦)) |
| 15 | 14 | rnmposs 32684 |
. . 3
⊢
(∀𝑥 ∈
𝔅ℝ ∀𝑦 ∈ 𝔅ℝ (𝑥 × 𝑦) ∈ 𝒫 (ℝ × ℝ)
→ ran (𝑥 ∈
𝔅ℝ, 𝑦 ∈ 𝔅ℝ ↦
(𝑥 × 𝑦)) ⊆ 𝒫 (ℝ
× ℝ)) |
| 16 | 13, 15 | ax-mp 5 |
. 2
⊢ ran
(𝑥 ∈
𝔅ℝ, 𝑦 ∈ 𝔅ℝ ↦
(𝑥 × 𝑦)) ⊆ 𝒫 (ℝ
× ℝ) |
| 17 | | unibrsiga 34187 |
. . . . . 6
⊢ ∪ 𝔅ℝ = ℝ |
| 18 | | brsigarn 34185 |
. . . . . . 7
⊢
𝔅ℝ ∈
(sigAlgebra‘ℝ) |
| 19 | | elrnsiga 34127 |
. . . . . . 7
⊢
(𝔅ℝ ∈ (sigAlgebra‘ℝ) →
𝔅ℝ ∈ ∪ ran
sigAlgebra) |
| 20 | | unielsiga 34129 |
. . . . . . 7
⊢
(𝔅ℝ ∈ ∪ ran
sigAlgebra → ∪ 𝔅ℝ
∈ 𝔅ℝ) |
| 21 | 18, 19, 20 | mp2b 10 |
. . . . . 6
⊢ ∪ 𝔅ℝ ∈
𝔅ℝ |
| 22 | 17, 21 | eqeltrri 2838 |
. . . . 5
⊢ ℝ
∈ 𝔅ℝ |
| 23 | | eqid 2737 |
. . . . 5
⊢ (ℝ
× ℝ) = (ℝ × ℝ) |
| 24 | | xpeq1 5699 |
. . . . . . 7
⊢ (𝑥 = ℝ → (𝑥 × 𝑦) = (ℝ × 𝑦)) |
| 25 | 24 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑥 = ℝ → ((ℝ
× ℝ) = (𝑥
× 𝑦) ↔ (ℝ
× ℝ) = (ℝ × 𝑦))) |
| 26 | | xpeq2 5706 |
. . . . . . 7
⊢ (𝑦 = ℝ → (ℝ
× 𝑦) = (ℝ
× ℝ)) |
| 27 | 26 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑦 = ℝ → ((ℝ
× ℝ) = (ℝ × 𝑦) ↔ (ℝ × ℝ) = (ℝ
× ℝ))) |
| 28 | 25, 27 | rspc2ev 3635 |
. . . . 5
⊢ ((ℝ
∈ 𝔅ℝ ∧ ℝ ∈
𝔅ℝ ∧ (ℝ × ℝ) = (ℝ ×
ℝ)) → ∃𝑥
∈ 𝔅ℝ ∃𝑦 ∈ 𝔅ℝ (ℝ
× ℝ) = (𝑥
× 𝑦)) |
| 29 | 22, 22, 23, 28 | mp3an 1463 |
. . . 4
⊢
∃𝑥 ∈
𝔅ℝ ∃𝑦 ∈ 𝔅ℝ (ℝ
× ℝ) = (𝑥
× 𝑦) |
| 30 | 14, 10 | elrnmpo 7569 |
. . . 4
⊢ ((ℝ
× ℝ) ∈ ran (𝑥 ∈ 𝔅ℝ, 𝑦 ∈
𝔅ℝ ↦ (𝑥 × 𝑦)) ↔ ∃𝑥 ∈ 𝔅ℝ
∃𝑦 ∈
𝔅ℝ (ℝ × ℝ) = (𝑥 × 𝑦)) |
| 31 | 29, 30 | mpbir 231 |
. . 3
⊢ (ℝ
× ℝ) ∈ ran (𝑥 ∈ 𝔅ℝ, 𝑦 ∈
𝔅ℝ ↦ (𝑥 × 𝑦)) |
| 32 | | elpwuni 5105 |
. . 3
⊢ ((ℝ
× ℝ) ∈ ran (𝑥 ∈ 𝔅ℝ, 𝑦 ∈
𝔅ℝ ↦ (𝑥 × 𝑦)) → (ran (𝑥 ∈ 𝔅ℝ, 𝑦 ∈
𝔅ℝ ↦ (𝑥 × 𝑦)) ⊆ 𝒫 (ℝ ×
ℝ) ↔ ∪ ran (𝑥 ∈ 𝔅ℝ, 𝑦 ∈
𝔅ℝ ↦ (𝑥 × 𝑦)) = (ℝ ×
ℝ))) |
| 33 | 31, 32 | ax-mp 5 |
. 2
⊢ (ran
(𝑥 ∈
𝔅ℝ, 𝑦 ∈ 𝔅ℝ ↦
(𝑥 × 𝑦)) ⊆ 𝒫 (ℝ
× ℝ) ↔ ∪ ran (𝑥 ∈ 𝔅ℝ, 𝑦 ∈
𝔅ℝ ↦ (𝑥 × 𝑦)) = (ℝ ×
ℝ)) |
| 34 | 16, 33 | mpbi 230 |
1
⊢ ∪ ran (𝑥 ∈ 𝔅ℝ, 𝑦 ∈
𝔅ℝ ↦ (𝑥 × 𝑦)) = (ℝ ×
ℝ) |