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 ∈ ℤ ⟼ x 2 n x + 1 2 n
dya2ioc.2 ⊢ R = u ∈ ran ⁡ I , v ∈ ran ⁡ I ⟼ u × v
Assertion sxbrsigalem5 ⊢ 𝛔 ⁡ J × t J ⊆ 𝔅 ℝ × s 𝔅 ℝ

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
2 dya2ioc.1 ⊢ I = x ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n
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 ⊢ u v g | u ∈ ran ⁡ I ∧ v ∈ ran ⁡ I ∧ g = u × v ⊆ u v g | u ∈ 𝔅 ℝ ∧ v ∈ 𝔅 ℝ ∧ g = u × v
17 df-mpo ⊢ u ∈ ran ⁡ I , v ∈ ran ⁡ I ⟼ u × v = u v g | u ∈ ran ⁡ I ∧ v ∈ ran ⁡ I ∧ g = u × v
18 3 17 eqtri ⊢ R = u v g | 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 = u v g | u ∈ 𝔅 ℝ ∧ v ∈ 𝔅 ℝ ∧ g = u × v
23 21 22 eqtri ⊢ e ∈ 𝔅 ℝ , f ∈ 𝔅 ℝ ⟼ e × f = u v g | 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 × t J = 𝛔 ⁡ 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 × t J ⊆ 𝔅 ℝ × s 𝔅 ℝ