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 𝐽 = ( topGen ‘ ran (,) )
dya2ioc.1 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
dya2ioc.2 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
Assertion sxbrsigalem5 ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( 𝔅 ×s 𝔅 )

Proof

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 𝔅 )