Metamath Proof Explorer


Theorem sxbrsigalem2

Description: The sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ) is a subset of the sigma-algebra generated by the closed half-spaces of ( RR X. RR ) . The proof goes by noting the fact that the dyadic rectangles are intersections of a 'vertical band' and an 'horizontal band', which themselves are differences of closed half-spaces. (Contributed by Thierry Arnoux, 17-Sep-2017)

Ref Expression
Hypotheses sxbrsiga.0 𝐽 = ( topGen ‘ ran (,) )
dya2ioc.1 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
dya2ioc.2 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
Assertion sxbrsigalem2 ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )

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 sxbrsigalem0 ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ℝ × ℝ )
6 4 5 eqtr4i ran 𝑅 = ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
7 vex 𝑢 ∈ V
8 vex 𝑣 ∈ V
9 7 8 xpex ( 𝑢 × 𝑣 ) ∈ V
10 3 9 elrnmpo ( 𝑑 ∈ ran 𝑅 ↔ ∃ 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 𝑑 = ( 𝑢 × 𝑣 ) )
11 simpr ( ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) ∧ 𝑑 = ( 𝑢 × 𝑣 ) ) → 𝑑 = ( 𝑢 × 𝑣 ) )
12 1 2 dya2icobrsiga ran 𝐼 ⊆ 𝔅
13 brsigasspwrn 𝔅 ⊆ 𝒫 ℝ
14 12 13 sstri ran 𝐼 ⊆ 𝒫 ℝ
15 14 sseli ( 𝑢 ∈ ran 𝐼𝑢 ∈ 𝒫 ℝ )
16 15 elpwid ( 𝑢 ∈ ran 𝐼𝑢 ⊆ ℝ )
17 14 sseli ( 𝑣 ∈ ran 𝐼𝑣 ∈ 𝒫 ℝ )
18 17 elpwid ( 𝑣 ∈ ran 𝐼𝑣 ⊆ ℝ )
19 xpinpreima2 ( ( 𝑢 ⊆ ℝ ∧ 𝑣 ⊆ ℝ ) → ( 𝑢 × 𝑣 ) = ( ( ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∩ ( ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ) )
20 16 18 19 syl2an ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) → ( 𝑢 × 𝑣 ) = ( ( ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∩ ( ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ) )
21 reex ℝ ∈ V
22 21 mptex ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∈ V
23 22 rnex ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∈ V
24 21 mptex ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ∈ V
25 24 rnex ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ∈ V
26 23 25 unex ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V
27 26 a1i ( ⊤ → ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V )
28 27 sgsiga ( ⊤ → ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ran sigAlgebra )
29 28 mptru ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ran sigAlgebra
30 29 a1i ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) → ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ran sigAlgebra )
31 1stpreima ( 𝑢 ⊆ ℝ → ( ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) = ( 𝑢 × ℝ ) )
32 16 31 syl ( 𝑢 ∈ ran 𝐼 → ( ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) = ( 𝑢 × ℝ ) )
33 ovex ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ V
34 2 33 elrnmpo ( 𝑢 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
35 simpr ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
36 35 xpeq1d ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑢 × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) )
37 simpl ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℤ )
38 37 zred ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ )
39 2rp 2 ∈ ℝ+
40 39 a1i ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 2 ∈ ℝ+ )
41 simpr ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
42 40 41 rpexpcld ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
43 38 42 rerpdivcld ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
44 43 rexrd ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* )
45 1red ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 1 ∈ ℝ )
46 38 45 readdcld ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 + 1 ) ∈ ℝ )
47 46 42 rerpdivcld ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
48 47 rexrd ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* )
49 pnfxr +∞ ∈ ℝ*
50 49 a1i ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → +∞ ∈ ℝ* )
51 38 lep1d ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ≤ ( 𝑥 + 1 ) )
52 38 46 42 51 lediv1dd ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) )
53 pnfge ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ +∞ )
54 48 53 syl ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ +∞ )
55 difico ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ +∞ ) ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
56 44 48 50 52 54 55 syl32anc ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
57 56 xpeq1d ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) )
58 difxp1 ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) × ℝ ) = ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∖ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) )
59 57 58 eqtr3di ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) = ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∖ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) )
60 29 a1i ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ran sigAlgebra )
61 ssun1 ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
62 eqid ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ )
63 oveq1 ( 𝑒 = ( 𝑥 / ( 2 ↑ 𝑛 ) ) → ( 𝑒 [,) +∞ ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) )
64 63 xpeq1d ( 𝑒 = ( 𝑥 / ( 2 ↑ 𝑛 ) ) → ( ( 𝑒 [,) +∞ ) × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) )
65 64 rspceeqv ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) → ∃ 𝑒 ∈ ℝ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) )
66 43 62 65 sylancl ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑒 ∈ ℝ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) )
67 eqid ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) = ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) )
68 ovex ( 𝑒 [,) +∞ ) ∈ V
69 68 21 xpex ( ( 𝑒 [,) +∞ ) × ℝ ) ∈ V
70 67 69 elrnmpti ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ↔ ∃ 𝑒 ∈ ℝ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) )
71 66 70 sylibr ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) )
72 61 71 sselid ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )
73 elsigagen ( ( ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ∧ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
74 26 72 73 sylancr ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
75 eqid ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ )
76 oveq1 ( 𝑒 = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) → ( 𝑒 [,) +∞ ) = ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) )
77 76 xpeq1d ( 𝑒 = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) → ( ( 𝑒 [,) +∞ ) × ℝ ) = ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) )
78 77 rspceeqv ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) → ∃ 𝑒 ∈ ℝ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) )
79 47 75 78 sylancl ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑒 ∈ ℝ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) )
80 67 69 elrnmpti ( ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ↔ ∃ 𝑒 ∈ ℝ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) )
81 79 80 sylibr ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) )
82 61 81 sselid ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )
83 elsigagen ( ( ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ∧ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) → ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
84 26 82 83 sylancr ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
85 difelsiga ( ( ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ran sigAlgebra ∧ ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∧ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) → ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∖ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
86 60 74 84 85 syl3anc ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∖ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
87 59 86 eqeltrd ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
88 87 adantr ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
89 36 88 eqeltrd ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑢 × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
90 89 ex ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → ( 𝑢 × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) )
91 90 rexlimivv ( ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑢 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → ( 𝑢 × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
92 34 91 sylbi ( 𝑢 ∈ ran 𝐼 → ( 𝑢 × ℝ ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
93 32 92 eqeltrd ( 𝑢 ∈ ran 𝐼 → ( ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
94 93 adantr ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) → ( ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
95 2ndpreima ( 𝑣 ⊆ ℝ → ( ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) = ( ℝ × 𝑣 ) )
96 18 95 syl ( 𝑣 ∈ ran 𝐼 → ( ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) = ( ℝ × 𝑣 ) )
97 2 33 elrnmpo ( 𝑣 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
98 simpr ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
99 98 xpeq2d ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ℝ × 𝑣 ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) )
100 56 xpeq2d ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) )
101 difxp2 ( ℝ × ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) = ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∖ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) )
102 100 101 eqtr3di ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) = ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∖ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) )
103 ssun2 ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
104 eqid ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) )
105 oveq1 ( 𝑓 = ( 𝑥 / ( 2 ↑ 𝑛 ) ) → ( 𝑓 [,) +∞ ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) )
106 105 xpeq2d ( 𝑓 = ( 𝑥 / ( 2 ↑ 𝑛 ) ) → ( ℝ × ( 𝑓 [,) +∞ ) ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) )
107 106 rspceeqv ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) → ∃ 𝑓 ∈ ℝ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) )
108 43 104 107 sylancl ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑓 ∈ ℝ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) )
109 eqid ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) = ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) )
110 ovex ( 𝑓 [,) +∞ ) ∈ V
111 21 110 xpex ( ℝ × ( 𝑓 [,) +∞ ) ) ∈ V
112 109 111 elrnmpti ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ↔ ∃ 𝑓 ∈ ℝ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) )
113 108 112 sylibr ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
114 103 113 sselid ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )
115 elsigagen ( ( ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ∧ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
116 26 114 115 sylancr ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
117 eqid ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) )
118 oveq1 ( 𝑓 = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) → ( 𝑓 [,) +∞ ) = ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) )
119 118 xpeq2d ( 𝑓 = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) → ( ℝ × ( 𝑓 [,) +∞ ) ) = ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) )
120 119 rspceeqv ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) → ∃ 𝑓 ∈ ℝ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) )
121 47 117 120 sylancl ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑓 ∈ ℝ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) )
122 109 111 elrnmpti ( ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ↔ ∃ 𝑓 ∈ ℝ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) )
123 121 122 sylibr ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
124 103 123 sselid ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )
125 elsigagen ( ( ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ∧ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) → ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
126 26 124 125 sylancr ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
127 difelsiga ( ( ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ran sigAlgebra ∧ ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∧ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) → ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∖ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
128 60 116 126 127 syl3anc ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∖ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
129 102 128 eqeltrd ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
130 129 adantr ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
131 99 130 eqeltrd ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ℝ × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
132 131 ex ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → ( ℝ × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) )
133 132 rexlimivv ( ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑣 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → ( ℝ × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
134 97 133 sylbi ( 𝑣 ∈ ran 𝐼 → ( ℝ × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
135 96 134 eqeltrd ( 𝑣 ∈ ran 𝐼 → ( ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
136 135 adantl ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) → ( ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
137 inelsiga ( ( ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∈ ran sigAlgebra ∧ ( ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∧ ( ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) → ( ( ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∩ ( ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
138 30 94 136 137 syl3anc ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) → ( ( ( 1st ↾ ( ℝ × ℝ ) ) “ 𝑢 ) ∩ ( ( 2nd ↾ ( ℝ × ℝ ) ) “ 𝑣 ) ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
139 20 138 eqeltrd ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) → ( 𝑢 × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
140 139 adantr ( ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) ∧ 𝑑 = ( 𝑢 × 𝑣 ) ) → ( 𝑢 × 𝑣 ) ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
141 11 140 eqeltrd ( ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) ∧ 𝑑 = ( 𝑢 × 𝑣 ) ) → 𝑑 ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
142 141 ex ( ( 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 ) → ( 𝑑 = ( 𝑢 × 𝑣 ) → 𝑑 ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ) )
143 142 rexlimivv ( ∃ 𝑢 ∈ ran 𝐼𝑣 ∈ ran 𝐼 𝑑 = ( 𝑢 × 𝑣 ) → 𝑑 ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
144 10 143 sylbi ( 𝑑 ∈ ran 𝑅𝑑 ∈ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
145 144 ssriv ran 𝑅 ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )
146 sigagenss2 ( ( ran 𝑅 = ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∧ ran 𝑅 ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ∧ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ∈ V ) → ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) )
147 6 145 26 146 mp3an ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )