Step |
Hyp |
Ref |
Expression |
1 |
|
sxbrsiga.0 |
⊢ 𝐽 = ( topGen ‘ ran (,) ) |
2 |
|
dya2ioc.1 |
⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) |
3 |
|
dya2ioc.2 |
⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) ) |
4 |
1 2 3
|
dya2iocucvr |
⊢ ∪ ran 𝑅 = ( ℝ × ℝ ) |
5 |
|
br2base |
⊢ ∪ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) = ( ℝ × ℝ ) |
6 |
4 5
|
eqtr4i |
⊢ ∪ ran 𝑅 = ∪ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) |
7 |
|
brsigarn |
⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) |
8 |
7
|
elexi |
⊢ 𝔅ℝ ∈ V |
9 |
8 8
|
mpoex |
⊢ ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ∈ V |
10 |
9
|
rnex |
⊢ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ∈ V |
11 |
1 2
|
dya2icobrsiga |
⊢ ran 𝐼 ⊆ 𝔅ℝ |
12 |
11
|
sseli |
⊢ ( 𝑢 ∈ ran 𝐼 → 𝑢 ∈ 𝔅ℝ ) |
13 |
11
|
sseli |
⊢ ( 𝑣 ∈ ran 𝐼 → 𝑣 ∈ 𝔅ℝ ) |
14 |
12 13
|
anim12i |
⊢ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) → ( 𝑢 ∈ 𝔅ℝ ∧ 𝑣 ∈ 𝔅ℝ ) ) |
15 |
14
|
anim1i |
⊢ ( ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑔 = ( 𝑢 × 𝑣 ) ) → ( ( 𝑢 ∈ 𝔅ℝ ∧ 𝑣 ∈ 𝔅ℝ ) ∧ 𝑔 = ( 𝑢 × 𝑣 ) ) ) |
16 |
15
|
ssoprab2i |
⊢ { 〈 〈 𝑢 , 𝑣 〉 , 𝑔 〉 ∣ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑔 = ( 𝑢 × 𝑣 ) ) } ⊆ { 〈 〈 𝑢 , 𝑣 〉 , 𝑔 〉 ∣ ( ( 𝑢 ∈ 𝔅ℝ ∧ 𝑣 ∈ 𝔅ℝ ) ∧ 𝑔 = ( 𝑢 × 𝑣 ) ) } |
17 |
|
df-mpo |
⊢ ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) ) = { 〈 〈 𝑢 , 𝑣 〉 , 𝑔 〉 ∣ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑔 = ( 𝑢 × 𝑣 ) ) } |
18 |
3 17
|
eqtri |
⊢ 𝑅 = { 〈 〈 𝑢 , 𝑣 〉 , 𝑔 〉 ∣ ( ( 𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼 ) ∧ 𝑔 = ( 𝑢 × 𝑣 ) ) } |
19 |
|
xpeq1 |
⊢ ( 𝑒 = 𝑢 → ( 𝑒 × 𝑓 ) = ( 𝑢 × 𝑓 ) ) |
20 |
|
xpeq2 |
⊢ ( 𝑓 = 𝑣 → ( 𝑢 × 𝑓 ) = ( 𝑢 × 𝑣 ) ) |
21 |
19 20
|
cbvmpov |
⊢ ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) = ( 𝑢 ∈ 𝔅ℝ , 𝑣 ∈ 𝔅ℝ ↦ ( 𝑢 × 𝑣 ) ) |
22 |
|
df-mpo |
⊢ ( 𝑢 ∈ 𝔅ℝ , 𝑣 ∈ 𝔅ℝ ↦ ( 𝑢 × 𝑣 ) ) = { 〈 〈 𝑢 , 𝑣 〉 , 𝑔 〉 ∣ ( ( 𝑢 ∈ 𝔅ℝ ∧ 𝑣 ∈ 𝔅ℝ ) ∧ 𝑔 = ( 𝑢 × 𝑣 ) ) } |
23 |
21 22
|
eqtri |
⊢ ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) = { 〈 〈 𝑢 , 𝑣 〉 , 𝑔 〉 ∣ ( ( 𝑢 ∈ 𝔅ℝ ∧ 𝑣 ∈ 𝔅ℝ ) ∧ 𝑔 = ( 𝑢 × 𝑣 ) ) } |
24 |
16 18 23
|
3sstr4i |
⊢ 𝑅 ⊆ ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) |
25 |
|
rnss |
⊢ ( 𝑅 ⊆ ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) → ran 𝑅 ⊆ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ) |
26 |
24 25
|
ax-mp |
⊢ ran 𝑅 ⊆ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) |
27 |
|
sssigagen2 |
⊢ ( ( ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ∈ V ∧ ran 𝑅 ⊆ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ) → ran 𝑅 ⊆ ( sigaGen ‘ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ) ) |
28 |
10 26 27
|
mp2an |
⊢ ran 𝑅 ⊆ ( sigaGen ‘ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ) |
29 |
|
sigagenss2 |
⊢ ( ( ∪ ran 𝑅 = ∪ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ∧ ran 𝑅 ⊆ ( sigaGen ‘ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ) ∧ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ∈ V ) → ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ) ) |
30 |
6 28 10 29
|
mp3an |
⊢ ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ) |
31 |
1 2 3
|
sxbrsigalem4 |
⊢ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) = ( sigaGen ‘ ran 𝑅 ) |
32 |
|
eqid |
⊢ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) = ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) |
33 |
32
|
sxval |
⊢ ( ( 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) ∧ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) ) → ( 𝔅ℝ ×s 𝔅ℝ ) = ( sigaGen ‘ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ) ) |
34 |
7 7 33
|
mp2an |
⊢ ( 𝔅ℝ ×s 𝔅ℝ ) = ( sigaGen ‘ ran ( 𝑒 ∈ 𝔅ℝ , 𝑓 ∈ 𝔅ℝ ↦ ( 𝑒 × 𝑓 ) ) ) |
35 |
30 31 34
|
3sstr4i |
⊢ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( 𝔅ℝ ×s 𝔅ℝ ) |