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 difxp1 ⊢ ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) × ℝ ) = ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∖ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) )
38 simpl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℤ )
39 38 zred ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ )
40 2rp ⊢ 2 ∈ ℝ+
41 40 a1i ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 2 ∈ ℝ+ )
42 simpr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
43 41 42 rpexpcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
44 39 43 rerpdivcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
45 44 rexrd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* )
46 1red ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 1 ∈ ℝ )
47 39 46 readdcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 + 1 ) ∈ ℝ )
48 47 43 rerpdivcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
49 48 rexrd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* )
50 pnfxr ⊢ +∞ ∈ ℝ*
51 50 a1i ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → +∞ ∈ ℝ* )
52 39 lep1d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ≤ ( 𝑥 + 1 ) )
53 39 47 43 52 lediv1dd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) )
54 pnfge ⊢ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ +∞ )
55 49 54 syl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ +∞ )
56 difico ⊢ ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ +∞ ) ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
57 45 49 51 53 55 56 syl32anc ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
58 57 xpeq1d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) × ℝ ) = ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) × ℝ ) )
59 37 58 syl5reqr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 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 44 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 sseldi ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝑥 / ( 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 48 75 78 sylancl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑒 ∈ ℝ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) )
80 67 69 elrnmpti ⊢ ( ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ↔ ∃ 𝑒 ∈ ℝ ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) = ( ( 𝑒 [,) +∞ ) × ℝ ) )
81 79 80 sylibr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) × ℝ ) ∈ ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) )
82 61 81 sseldi ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( ( 𝑥 + 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 difxp2 ⊢ ( ℝ × ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) = ( ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∖ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) )
101 57 xpeq2d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ∖ ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ) = ( ℝ × ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) )
102 100 101 syl5reqr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 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 44 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 sseldi ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( 𝑥 / ( 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 48 117 120 sylancl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑓 ∈ ℝ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) )
122 109 111 elrnmpti ⊢ ( ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ↔ ∃ 𝑓 ∈ ℝ ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) = ( ℝ × ( 𝑓 [,) +∞ ) ) )
123 121 122 sylibr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) [,) +∞ ) ) ∈ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) )
124 103 123 sseldi ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ℝ × ( ( ( 𝑥 + 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 ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )