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