Metamath Proof Explorer

Theorem sxbrsigalem5

Description: First direction for sxbrsiga . (Contributed by Thierry Arnoux, 22-Sep-2017) (Revised by Thierry Arnoux, 11-Oct-2017)

Ref Expression
Hypotheses sxbrsiga.0 ⊢J=topGen⁡ran⁡.
dya2ioc.1 ⊢I=x∈ℤ,n∈ℤ⟼x2nx+12n
dya2ioc.2 ⊢R=u∈ran⁡I,v∈ran⁡I⟼u×v
Assertion sxbrsigalem5 ⊢𝛔⁡J×tJ⊆𝔅ℝ×s𝔅ℝ

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢J=topGen⁡ran⁡.
2 dya2ioc.1 ⊢I=x∈ℤ,n∈ℤ⟼x2nx+12n
3 dya2ioc.2 ⊢R=u∈ran⁡I,v∈ran⁡I⟼u×v
4 1 2 3 dya2iocucvr ⊢⋃ran⁡R=ℝ2
5 br2base ⊢⋃ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f=ℝ2
6 4 5 eqtr4i ⊢⋃ran⁡R=⋃ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
7 brsigarn ⊢𝔅ℝ∈sigAlgebra⁡ℝ
8 7 elexi ⊢𝔅ℝ∈V
9 8 8 mpoex ⊢e∈𝔅ℝ,f∈𝔅ℝ⟼e×f∈V
10 9 rnex ⊢ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f∈V
11 1 2 dya2icobrsiga ⊢ran⁡I⊆𝔅ℝ
12 11 sseli ⊢u∈ran⁡I→u∈𝔅ℝ
13 11 sseli ⊢v∈ran⁡I→v∈𝔅ℝ
14 12 13 anim12i ⊢u∈ran⁡I∧v∈ran⁡I→u∈𝔅ℝ∧v∈𝔅ℝ
15 14 anim1i ⊢u∈ran⁡I∧v∈ran⁡I∧g=u×v→u∈𝔅ℝ∧v∈𝔅ℝ∧g=u×v
16 15 ssoprab2i ⊢uvg|u∈ran⁡I∧v∈ran⁡I∧g=u×v⊆uvg|u∈𝔅ℝ∧v∈𝔅ℝ∧g=u×v
17 df-mpo ⊢u∈ran⁡I,v∈ran⁡I⟼u×v=uvg|u∈ran⁡I∧v∈ran⁡I∧g=u×v
18 3 17 eqtri ⊢R=uvg|u∈ran⁡I∧v∈ran⁡I∧g=u×v
19 xpeq1 ⊢e=u→e×f=u×f
20 xpeq2 ⊢f=v→u×f=u×v
21 19 20 cbvmpov ⊢e∈𝔅ℝ,f∈𝔅ℝ⟼e×f=u∈𝔅ℝ,v∈𝔅ℝ⟼u×v
22 df-mpo ⊢u∈𝔅ℝ,v∈𝔅ℝ⟼u×v=uvg|u∈𝔅ℝ∧v∈𝔅ℝ∧g=u×v
23 21 22 eqtri ⊢e∈𝔅ℝ,f∈𝔅ℝ⟼e×f=uvg|u∈𝔅ℝ∧v∈𝔅ℝ∧g=u×v
24 16 18 23 3sstr4i ⊢R⊆e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
25 rnss ⊢R⊆e∈𝔅ℝ,f∈𝔅ℝ⟼e×f→ran⁡R⊆ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
26 24 25 ax-mp ⊢ran⁡R⊆ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
27 sssigagen2 ⊢ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f∈V∧ran⁡R⊆ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f→ran⁡R⊆𝛔⁡ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
28 10 26 27 mp2an ⊢ran⁡R⊆𝛔⁡ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
29 sigagenss2 ⊢⋃ran⁡R=⋃ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f∧ran⁡R⊆𝛔⁡ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f∧ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f∈V→𝛔⁡ran⁡R⊆𝛔⁡ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
30 6 28 10 29 mp3an ⊢𝛔⁡ran⁡R⊆𝛔⁡ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
31 1 2 3 sxbrsigalem4 ⊢𝛔⁡J×tJ=𝛔⁡ran⁡R
32 eqid ⊢ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f=ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
33 32 sxval ⊢𝔅ℝ∈sigAlgebra⁡ℝ∧𝔅ℝ∈sigAlgebra⁡ℝ→𝔅ℝ×s𝔅ℝ=𝛔⁡ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
34 7 7 33 mp2an ⊢𝔅ℝ×s𝔅ℝ=𝛔⁡ran⁡e∈𝔅ℝ,f∈𝔅ℝ⟼e×f
35 30 31 34 3sstr4i ⊢𝛔⁡J×tJ⊆𝔅ℝ×s𝔅ℝ