Step | Hyp | Ref
| Expression |
1 | | brsigarn 32152 |
. . . 4
⊢
𝔅ℝ ∈
(sigAlgebra‘ℝ) |
2 | | eqid 2738 |
. . . . 5
⊢ ran
(𝑒 ∈
𝔅ℝ, 𝑓 ∈ 𝔅ℝ ↦
(𝑒 × 𝑓)) = ran (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓)) |
3 | 2 | sxval 32158 |
. . . 4
⊢
((𝔅ℝ ∈ (sigAlgebra‘ℝ) ∧
𝔅ℝ ∈ (sigAlgebra‘ℝ)) →
(𝔅ℝ ×s 𝔅ℝ) =
(sigaGen‘ran (𝑒
∈ 𝔅ℝ, 𝑓 ∈ 𝔅ℝ ↦
(𝑒 × 𝑓)))) |
4 | 1, 1, 3 | mp2an 689 |
. . 3
⊢
(𝔅ℝ ×s
𝔅ℝ) = (sigaGen‘ran (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓))) |
5 | | br2base 32236 |
. . . . 5
⊢ ∪ ran (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓)) = (ℝ ×
ℝ) |
6 | | sxbrsiga.0 |
. . . . . 6
⊢ 𝐽 = (topGen‘ran
(,)) |
7 | 6 | tpr2uni 31855 |
. . . . 5
⊢ ∪ (𝐽
×t 𝐽) =
(ℝ × ℝ) |
8 | 5, 7 | eqtr4i 2769 |
. . . 4
⊢ ∪ ran (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓)) = ∪ (𝐽 ×t 𝐽) |
9 | | brsigasspwrn 32153 |
. . . . . . . . . 10
⊢
𝔅ℝ ⊆ 𝒫 ℝ |
10 | 9 | sseli 3917 |
. . . . . . . . 9
⊢ (𝑒 ∈
𝔅ℝ → 𝑒 ∈ 𝒫 ℝ) |
11 | 10 | elpwid 4544 |
. . . . . . . 8
⊢ (𝑒 ∈
𝔅ℝ → 𝑒 ⊆ ℝ) |
12 | 9 | sseli 3917 |
. . . . . . . . 9
⊢ (𝑓 ∈
𝔅ℝ → 𝑓 ∈ 𝒫 ℝ) |
13 | 12 | elpwid 4544 |
. . . . . . . 8
⊢ (𝑓 ∈
𝔅ℝ → 𝑓 ⊆ ℝ) |
14 | | xpinpreima2 31857 |
. . . . . . . 8
⊢ ((𝑒 ⊆ ℝ ∧ 𝑓 ⊆ ℝ) → (𝑒 × 𝑓) = ((◡(1st ↾ (ℝ ×
ℝ)) “ 𝑒) ∩
(◡(2nd ↾ (ℝ
× ℝ)) “ 𝑓))) |
15 | 11, 13, 14 | syl2an 596 |
. . . . . . 7
⊢ ((𝑒 ∈
𝔅ℝ ∧ 𝑓 ∈ 𝔅ℝ) →
(𝑒 × 𝑓) = ((◡(1st ↾ (ℝ ×
ℝ)) “ 𝑒) ∩
(◡(2nd ↾ (ℝ
× ℝ)) “ 𝑓))) |
16 | 6 | tpr2tp 31854 |
. . . . . . . . . 10
⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ
× ℝ)) |
17 | | sigagensiga 32109 |
. . . . . . . . . 10
⊢ ((𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ
× ℝ)) → (sigaGen‘(𝐽 ×t 𝐽)) ∈ (sigAlgebra‘∪ (𝐽
×t 𝐽))) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . 9
⊢
(sigaGen‘(𝐽
×t 𝐽))
∈ (sigAlgebra‘∪ (𝐽 ×t 𝐽)) |
19 | | elrnsiga 32094 |
. . . . . . . . 9
⊢
((sigaGen‘(𝐽
×t 𝐽))
∈ (sigAlgebra‘∪ (𝐽 ×t 𝐽)) → (sigaGen‘(𝐽 ×t 𝐽)) ∈ ∪ ran
sigAlgebra) |
20 | 18, 19 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑒 ∈
𝔅ℝ ∧ 𝑓 ∈ 𝔅ℝ) →
(sigaGen‘(𝐽
×t 𝐽))
∈ ∪ ran sigAlgebra) |
21 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑒 ∈
𝔅ℝ → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ ×
ℝ))) |
22 | 21 | sgsiga 32110 |
. . . . . . . . . 10
⊢ (𝑒 ∈
𝔅ℝ → (sigaGen‘(𝐽 ×t 𝐽)) ∈ ∪ ran
sigAlgebra) |
23 | | elrnsiga 32094 |
. . . . . . . . . . 11
⊢
(𝔅ℝ ∈ (sigAlgebra‘ℝ) →
𝔅ℝ ∈ ∪ ran
sigAlgebra) |
24 | 1, 23 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝑒 ∈
𝔅ℝ → 𝔅ℝ ∈ ∪ ran sigAlgebra) |
25 | | retopon 23927 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
26 | 6, 25 | eqeltri 2835 |
. . . . . . . . . . . . 13
⊢ 𝐽 ∈
(TopOn‘ℝ) |
27 | | tx1cn 22760 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘ℝ)
∧ 𝐽 ∈
(TopOn‘ℝ)) → (1st ↾ (ℝ ×
ℝ)) ∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
28 | 26, 26, 27 | mp2an 689 |
. . . . . . . . . . . 12
⊢
(1st ↾ (ℝ × ℝ)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑒 ∈
𝔅ℝ → (1st ↾ (ℝ ×
ℝ)) ∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
30 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ (𝑒 ∈
𝔅ℝ → (sigaGen‘(𝐽 ×t 𝐽)) = (sigaGen‘(𝐽 ×t 𝐽))) |
31 | | df-brsiga 32150 |
. . . . . . . . . . . . 13
⊢
𝔅ℝ = (sigaGen‘(topGen‘ran
(,))) |
32 | 6 | fveq2i 6777 |
. . . . . . . . . . . . 13
⊢
(sigaGen‘𝐽) =
(sigaGen‘(topGen‘ran (,))) |
33 | 31, 32 | eqtr4i 2769 |
. . . . . . . . . . . 12
⊢
𝔅ℝ = (sigaGen‘𝐽) |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑒 ∈
𝔅ℝ → 𝔅ℝ =
(sigaGen‘𝐽)) |
35 | 29, 30, 34 | cnmbfm 32230 |
. . . . . . . . . 10
⊢ (𝑒 ∈
𝔅ℝ → (1st ↾ (ℝ ×
ℝ)) ∈ ((sigaGen‘(𝐽 ×t 𝐽))MblFnM𝔅ℝ)) |
36 | | id 22 |
. . . . . . . . . 10
⊢ (𝑒 ∈
𝔅ℝ → 𝑒 ∈
𝔅ℝ) |
37 | 22, 24, 35, 36 | mbfmcnvima 32224 |
. . . . . . . . 9
⊢ (𝑒 ∈
𝔅ℝ → (◡(1st ↾ (ℝ ×
ℝ)) “ 𝑒) ∈
(sigaGen‘(𝐽
×t 𝐽))) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢ ((𝑒 ∈
𝔅ℝ ∧ 𝑓 ∈ 𝔅ℝ) →
(◡(1st ↾ (ℝ
× ℝ)) “ 𝑒) ∈ (sigaGen‘(𝐽 ×t 𝐽))) |
39 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑓 ∈
𝔅ℝ → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ ×
ℝ))) |
40 | 39 | sgsiga 32110 |
. . . . . . . . . 10
⊢ (𝑓 ∈
𝔅ℝ → (sigaGen‘(𝐽 ×t 𝐽)) ∈ ∪ ran
sigAlgebra) |
41 | 1, 23 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝑓 ∈
𝔅ℝ → 𝔅ℝ ∈ ∪ ran sigAlgebra) |
42 | | tx2cn 22761 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘ℝ)
∧ 𝐽 ∈
(TopOn‘ℝ)) → (2nd ↾ (ℝ ×
ℝ)) ∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
43 | 26, 26, 42 | mp2an 689 |
. . . . . . . . . . . 12
⊢
(2nd ↾ (ℝ × ℝ)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑓 ∈
𝔅ℝ → (2nd ↾ (ℝ ×
ℝ)) ∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
45 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ (𝑓 ∈
𝔅ℝ → (sigaGen‘(𝐽 ×t 𝐽)) = (sigaGen‘(𝐽 ×t 𝐽))) |
46 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑓 ∈
𝔅ℝ → 𝔅ℝ =
(sigaGen‘𝐽)) |
47 | 44, 45, 46 | cnmbfm 32230 |
. . . . . . . . . 10
⊢ (𝑓 ∈
𝔅ℝ → (2nd ↾ (ℝ ×
ℝ)) ∈ ((sigaGen‘(𝐽 ×t 𝐽))MblFnM𝔅ℝ)) |
48 | | id 22 |
. . . . . . . . . 10
⊢ (𝑓 ∈
𝔅ℝ → 𝑓 ∈
𝔅ℝ) |
49 | 40, 41, 47, 48 | mbfmcnvima 32224 |
. . . . . . . . 9
⊢ (𝑓 ∈
𝔅ℝ → (◡(2nd ↾ (ℝ ×
ℝ)) “ 𝑓) ∈
(sigaGen‘(𝐽
×t 𝐽))) |
50 | 49 | adantl 482 |
. . . . . . . 8
⊢ ((𝑒 ∈
𝔅ℝ ∧ 𝑓 ∈ 𝔅ℝ) →
(◡(2nd ↾ (ℝ
× ℝ)) “ 𝑓) ∈ (sigaGen‘(𝐽 ×t 𝐽))) |
51 | | inelsiga 32103 |
. . . . . . . 8
⊢
(((sigaGen‘(𝐽
×t 𝐽))
∈ ∪ ran sigAlgebra ∧ (◡(1st ↾ (ℝ ×
ℝ)) “ 𝑒) ∈
(sigaGen‘(𝐽
×t 𝐽))
∧ (◡(2nd ↾
(ℝ × ℝ)) “ 𝑓) ∈ (sigaGen‘(𝐽 ×t 𝐽))) → ((◡(1st ↾ (ℝ ×
ℝ)) “ 𝑒) ∩
(◡(2nd ↾ (ℝ
× ℝ)) “ 𝑓)) ∈ (sigaGen‘(𝐽 ×t 𝐽))) |
52 | 20, 38, 50, 51 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝑒 ∈
𝔅ℝ ∧ 𝑓 ∈ 𝔅ℝ) →
((◡(1st ↾ (ℝ
× ℝ)) “ 𝑒) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ 𝑓))
∈ (sigaGen‘(𝐽
×t 𝐽))) |
53 | 15, 52 | eqeltrd 2839 |
. . . . . 6
⊢ ((𝑒 ∈
𝔅ℝ ∧ 𝑓 ∈ 𝔅ℝ) →
(𝑒 × 𝑓) ∈ (sigaGen‘(𝐽 ×t 𝐽))) |
54 | 53 | rgen2 3120 |
. . . . 5
⊢
∀𝑒 ∈
𝔅ℝ ∀𝑓 ∈ 𝔅ℝ (𝑒 × 𝑓) ∈ (sigaGen‘(𝐽 ×t 𝐽)) |
55 | | eqid 2738 |
. . . . . 6
⊢ (𝑒 ∈
𝔅ℝ, 𝑓 ∈ 𝔅ℝ ↦
(𝑒 × 𝑓)) = (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓)) |
56 | 55 | rnmposs 31011 |
. . . . 5
⊢
(∀𝑒 ∈
𝔅ℝ ∀𝑓 ∈ 𝔅ℝ (𝑒 × 𝑓) ∈ (sigaGen‘(𝐽 ×t 𝐽)) → ran (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓)) ⊆ (sigaGen‘(𝐽 ×t 𝐽))) |
57 | 54, 56 | ax-mp 5 |
. . . 4
⊢ ran
(𝑒 ∈
𝔅ℝ, 𝑓 ∈ 𝔅ℝ ↦
(𝑒 × 𝑓)) ⊆ (sigaGen‘(𝐽 ×t 𝐽)) |
58 | | sigagenss2 32118 |
. . . 4
⊢ ((∪ ran (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓)) = ∪ (𝐽 ×t 𝐽) ∧ ran (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓)) ⊆ (sigaGen‘(𝐽 ×t 𝐽)) ∧ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ ×
ℝ))) → (sigaGen‘ran (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓))) ⊆ (sigaGen‘(𝐽 ×t 𝐽))) |
59 | 8, 57, 16, 58 | mp3an 1460 |
. . 3
⊢
(sigaGen‘ran (𝑒 ∈ 𝔅ℝ, 𝑓 ∈
𝔅ℝ ↦ (𝑒 × 𝑓))) ⊆ (sigaGen‘(𝐽 ×t 𝐽)) |
60 | 4, 59 | eqsstri 3955 |
. 2
⊢
(𝔅ℝ ×s
𝔅ℝ) ⊆ (sigaGen‘(𝐽 ×t 𝐽)) |
61 | 6 | sxbrsigalem6 32256 |
. 2
⊢
(sigaGen‘(𝐽
×t 𝐽))
⊆ (𝔅ℝ ×s
𝔅ℝ) |
62 | 60, 61 | eqssi 3937 |
1
⊢
(𝔅ℝ ×s
𝔅ℝ) = (sigaGen‘(𝐽 ×t 𝐽)) |