Metamath Proof Explorer


Theorem opnmbllem

Description: Lemma for opnmbl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
Assertion opnmbllem ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ∈ dom vol )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 fveq2 ( 𝑧 = 𝑤 → ( [,] ‘ 𝑧 ) = ( [,] ‘ 𝑤 ) )
3 2 sseq1d ( 𝑧 = 𝑤 → ( ( [,] ‘ 𝑧 ) ⊆ 𝐴 ↔ ( [,] ‘ 𝑤 ) ⊆ 𝐴 ) )
4 3 elrab ( 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ↔ ( 𝑤 ∈ ran 𝐹 ∧ ( [,] ‘ 𝑤 ) ⊆ 𝐴 ) )
5 simprr ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ ( 𝑤 ∈ ran 𝐹 ∧ ( [,] ‘ 𝑤 ) ⊆ 𝐴 ) ) → ( [,] ‘ 𝑤 ) ⊆ 𝐴 )
6 fvex ( [,] ‘ 𝑤 ) ∈ V
7 6 elpw ( ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 ↔ ( [,] ‘ 𝑤 ) ⊆ 𝐴 )
8 5 7 sylibr ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ ( 𝑤 ∈ ran 𝐹 ∧ ( [,] ‘ 𝑤 ) ⊆ 𝐴 ) ) → ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 )
9 4 8 sylan2b ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) → ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 )
10 9 ralrimiva ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ∀ 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 )
11 iccf [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
12 ffun ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → Fun [,] )
13 11 12 ax-mp Fun [,]
14 ssrab2 { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ ran 𝐹
15 1 dyadf 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) )
16 frn ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) )
17 15 16 ax-mp ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) )
18 inss2 ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
19 rexpssxrxp ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
20 18 19 sstri ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
21 17 20 sstri ran 𝐹 ⊆ ( ℝ* × ℝ* )
22 14 21 sstri { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ ( ℝ* × ℝ* )
23 11 fdmi dom [,] = ( ℝ* × ℝ* )
24 22 23 sseqtrri { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ dom [,]
25 funimass4 ( ( Fun [,] ∧ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ dom [,] ) → ( ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝒫 𝐴 ↔ ∀ 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 ) )
26 13 24 25 mp2an ( ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝒫 𝐴 ↔ ∀ 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 )
27 10 26 sylibr ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝒫 𝐴 )
28 sspwuni ( ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝒫 𝐴 ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝐴 )
29 27 28 sylib ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝐴 )
30 eqid ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
31 30 rexmet ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
32 eqid ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
33 30 32 tgioo ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
34 33 mopni2 ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴 )
35 31 34 mp3an1 ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴 )
36 elssuni ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ( topGen ‘ ran (,) ) )
37 uniretop ℝ = ( topGen ‘ ran (,) )
38 36 37 sseqtrrdi ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ⊆ ℝ )
39 38 sselda ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) → 𝑤 ∈ ℝ )
40 rpre ( 𝑟 ∈ ℝ+𝑟 ∈ ℝ )
41 30 bl2ioo ( ( 𝑤 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
42 39 40 41 syl2an ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
43 42 sseq1d ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴 ↔ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) )
44 2re 2 ∈ ℝ
45 1lt2 1 < 2
46 expnlbnd ( ( 𝑟 ∈ ℝ+ ∧ 2 ∈ ℝ ∧ 1 < 2 ) → ∃ 𝑛 ∈ ℕ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 )
47 44 45 46 mp3an23 ( 𝑟 ∈ ℝ+ → ∃ 𝑛 ∈ ℕ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 )
48 47 ad2antrl ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 )
49 39 ad2antrr ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ∈ ℝ )
50 2nn 2 ∈ ℕ
51 nnnn0 ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
52 51 ad2antrl ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑛 ∈ ℕ0 )
53 nnexpcl ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
54 50 52 53 sylancr ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
55 54 nnred ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
56 49 55 remulcld ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∈ ℝ )
57 fllelt ( ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∧ ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ) )
58 56 57 syl ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∧ ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ) )
59 58 simpld ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) )
60 reflcl ( ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
61 56 60 syl ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
62 54 nngt0d ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 0 < ( 2 ↑ 𝑛 ) )
63 ledivmul2 ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ ( ( 2 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑛 ) ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤 ↔ ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) )
64 61 49 55 62 63 syl112anc ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤 ↔ ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) )
65 59 64 mpbird ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤 )
66 peano2re ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ∈ ℝ )
67 61 66 syl ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ∈ ℝ )
68 67 54 nndivred ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
69 58 simprd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) )
70 ltmuldiv ( ( 𝑤 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ∈ ℝ ∧ ( ( 2 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑛 ) ) ) → ( ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ↔ 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
71 49 67 55 62 70 syl112anc ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ↔ 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
72 69 71 mpbid ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) )
73 49 68 72 ltled ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ≤ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) )
74 61 54 nndivred ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
75 elicc2 ( ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ ) → ( 𝑤 ∈ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤𝑤 ≤ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) )
76 74 68 75 syl2anc ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 ∈ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤𝑤 ≤ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) )
77 49 65 73 76 mpbir3and ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ∈ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
78 56 flcld ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℤ )
79 1 dyadval ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℤ ∧ 𝑛 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) = ⟨ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) , ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ⟩ )
80 78 52 79 syl2anc ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) = ⟨ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) , ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ⟩ )
81 80 fveq2d ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) = ( [,] ‘ ⟨ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) , ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ⟩ ) )
82 df-ov ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) = ( [,] ‘ ⟨ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) , ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ⟩ )
83 81 82 eqtr4di ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) = ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
84 77 83 eleqtrrd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ∈ ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) )
85 fveq2 ( 𝑧 = ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) → ( [,] ‘ 𝑧 ) = ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) )
86 85 sseq1d ( 𝑧 = ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) → ( ( [,] ‘ 𝑧 ) ⊆ 𝐴 ↔ ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ⊆ 𝐴 ) )
87 ffn ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 Fn ( ℤ × ℕ0 ) )
88 15 87 ax-mp 𝐹 Fn ( ℤ × ℕ0 )
89 fnovrn ( ( 𝐹 Fn ( ℤ × ℕ0 ) ∧ ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℤ ∧ 𝑛 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ ran 𝐹 )
90 88 78 52 89 mp3an2i ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ ran 𝐹 )
91 simplrl ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑟 ∈ ℝ+ )
92 91 rpred ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑟 ∈ ℝ )
93 49 92 resubcld ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤𝑟 ) ∈ ℝ )
94 93 rexrd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤𝑟 ) ∈ ℝ* )
95 49 92 readdcld ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 + 𝑟 ) ∈ ℝ )
96 95 rexrd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 + 𝑟 ) ∈ ℝ* )
97 74 92 readdcld ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) ∈ ℝ )
98 61 recnd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℂ )
99 1cnd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 1 ∈ ℂ )
100 55 recnd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
101 54 nnne0d ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 2 ↑ 𝑛 ) ≠ 0 )
102 98 99 100 101 divdird ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) = ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + ( 1 / ( 2 ↑ 𝑛 ) ) ) )
103 54 nnrecred ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 1 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
104 simprr ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 )
105 103 92 74 104 ltadd2dd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + ( 1 / ( 2 ↑ 𝑛 ) ) ) < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) )
106 102 105 eqbrtrd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) )
107 49 68 97 72 106 lttrd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) )
108 49 92 74 ltsubaddd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( 𝑤𝑟 ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ↔ 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) ) )
109 107 108 mpbird ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤𝑟 ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) )
110 49 103 readdcld ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
111 74 49 103 65 leadd1dd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + ( 1 / ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 + ( 1 / ( 2 ↑ 𝑛 ) ) ) )
112 102 111 eqbrtrd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ ( 𝑤 + ( 1 / ( 2 ↑ 𝑛 ) ) ) )
113 103 92 49 104 ltadd2dd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 + ( 1 / ( 2 ↑ 𝑛 ) ) ) < ( 𝑤 + 𝑟 ) )
114 68 110 95 112 113 lelttrd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) < ( 𝑤 + 𝑟 ) )
115 iccssioo ( ( ( ( 𝑤𝑟 ) ∈ ℝ* ∧ ( 𝑤 + 𝑟 ) ∈ ℝ* ) ∧ ( ( 𝑤𝑟 ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ∧ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) < ( 𝑤 + 𝑟 ) ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ⊆ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
116 94 96 109 114 115 syl22anc ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ⊆ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
117 83 116 eqsstrd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ⊆ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
118 simplrr ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 )
119 117 118 sstrd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ⊆ 𝐴 )
120 86 90 119 elrabd ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } )
121 funfvima2 ( ( Fun [,] ∧ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ dom [,] ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∈ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) )
122 13 24 121 mp2an ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∈ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
123 120 122 syl ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∈ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
124 elunii ( ( 𝑤 ∈ ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∧ ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∈ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) → 𝑤 ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
125 84 123 124 syl2anc ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
126 48 125 rexlimddv ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) → 𝑤 ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
127 126 expr ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( ( 𝑤𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴𝑤 ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) )
128 43 127 sylbid ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴𝑤 ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) )
129 128 rexlimdva ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴𝑤 ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) )
130 35 129 mpd ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤𝐴 ) → 𝑤 ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
131 29 130 eqelssd ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) = 𝐴 )
132 fveq2 ( 𝑐 = 𝑎 → ( [,] ‘ 𝑐 ) = ( [,] ‘ 𝑎 ) )
133 132 sseq1d ( 𝑐 = 𝑎 → ( ( [,] ‘ 𝑐 ) ⊆ ( [,] ‘ 𝑏 ) ↔ ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑏 ) ) )
134 equequ1 ( 𝑐 = 𝑎 → ( 𝑐 = 𝑏𝑎 = 𝑏 ) )
135 133 134 imbi12d ( 𝑐 = 𝑎 → ( ( ( [,] ‘ 𝑐 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑐 = 𝑏 ) ↔ ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
136 135 ralbidv ( 𝑐 = 𝑎 → ( ∀ 𝑏 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑐 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑐 = 𝑏 ) ↔ ∀ 𝑏 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
137 136 cbvrabv { 𝑐 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ∣ ∀ 𝑏 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑐 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑐 = 𝑏 ) } = { 𝑎 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ∣ ∀ 𝑏 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑎 = 𝑏 ) }
138 14 a1i ( 𝐴 ∈ ( topGen ‘ ran (,) ) → { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ ran 𝐹 )
139 1 137 138 dyadmbl ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ∈ dom vol )
140 131 139 eqeltrrd ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ∈ dom vol )