# Metamath Proof Explorer

## Theorem opnmbllem

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

Ref Expression
Hypothesis dyadmbl.1 $⊢ F = x ∈ ℤ , y ∈ ℕ 0 ⟼ x 2 y x + 1 2 y$
Assertion opnmbllem $⊢ A ∈ topGen ⁡ ran ⁡ . → A ∈ dom ⁡ vol$

### Proof

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