Theorem sxbrsigalem6

Description: First direction for sxbrsiga , same as sxbrsigalem6, dealing with the antecedents. (Contributed by Thierry Arnoux, 10-Oct-2017)

	Ref	Expression
Hypothesis	sxbrsiga.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
Assertion	sxbrsigalem6	⊢ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( 𝔅ℝ ×s 𝔅ℝ )

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		oveq1	⊢ ( 𝑎 = 𝑥 → ( 𝑎 / ( 2 ↑ 𝑚 ) ) = ( 𝑥 / ( 2 ↑ 𝑚 ) ) )
3		oveq1	⊢ ( 𝑎 = 𝑥 → ( 𝑎 + 1 ) = ( 𝑥 + 1 ) )
4	3	oveq1d	⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 + 1 ) / ( 2 ↑ 𝑚 ) ) = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑚 ) ) )
5	2 4	oveq12d	⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑎 + 1 ) / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑥 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑚 ) ) ) )
6		oveq2	⊢ ( 𝑚 = 𝑛 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑛 ) )
7	6	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 𝑥 / ( 2 ↑ 𝑚 ) ) = ( 𝑥 / ( 2 ↑ 𝑛 ) ) )
8	6	oveq2d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑚 ) ) = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) )
9	7 8	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑥 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
10	5 9	cbvmpov	⊢ ( 𝑎 ∈ ℤ , 𝑚 ∈ ℤ ↦ ( ( 𝑎 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑎 + 1 ) / ( 2 ↑ 𝑚 ) ) ) ) = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
11		eqid	⊢ ( 𝑢 ∈ ran ( 𝑎 ∈ ℤ , 𝑚 ∈ ℤ ↦ ( ( 𝑎 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑎 + 1 ) / ( 2 ↑ 𝑚 ) ) ) ) , 𝑣 ∈ ran ( 𝑎 ∈ ℤ , 𝑚 ∈ ℤ ↦ ( ( 𝑎 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑎 + 1 ) / ( 2 ↑ 𝑚 ) ) ) ) ↦ ( 𝑢 × 𝑣 ) ) = ( 𝑢 ∈ ran ( 𝑎 ∈ ℤ , 𝑚 ∈ ℤ ↦ ( ( 𝑎 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑎 + 1 ) / ( 2 ↑ 𝑚 ) ) ) ) , 𝑣 ∈ ran ( 𝑎 ∈ ℤ , 𝑚 ∈ ℤ ↦ ( ( 𝑎 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑎 + 1 ) / ( 2 ↑ 𝑚 ) ) ) ) ↦ ( 𝑢 × 𝑣 ) )
12	1 10 11	sxbrsigalem5	⊢ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( 𝔅ℝ ×s 𝔅ℝ )