Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  opnmbllem0 Structured version   Visualization version   GIF version

Theorem opnmbllem0 33677
 Description: Lemma for ismblfin 33682; could also be used to shorten proof of opnmbllem 23490. (Contributed by Brendan Leahy, 13-Jul-2018.)
Assertion
Ref Expression
opnmbllem0 (𝐴 ∈ (topGen‘ran (,)) → ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴)
Distinct variable group:   𝑥,𝑦,𝑧,𝐴

Proof of Theorem opnmbllem0
Dummy variables 𝑛 𝑟 𝑠 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6304 . . . . . . . 8 (𝑧 = 𝑤 → ([,]‘𝑧) = ([,]‘𝑤))
21sseq1d 3738 . . . . . . 7 (𝑧 = 𝑤 → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘𝑤) ⊆ 𝐴))
32elrab 3469 . . . . . 6 (𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ↔ (𝑤 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∧ ([,]‘𝑤) ⊆ 𝐴))
4 simprr 813 . . . . . . 7 ((𝐴 ∈ (topGen‘ran (,)) ∧ (𝑤 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ⊆ 𝐴)
5 fvex 6314 . . . . . . . 8 ([,]‘𝑤) ∈ V
65elpw 4272 . . . . . . 7 (([,]‘𝑤) ∈ 𝒫 𝐴 ↔ ([,]‘𝑤) ⊆ 𝐴)
74, 6sylibr 224 . . . . . 6 ((𝐴 ∈ (topGen‘ran (,)) ∧ (𝑤 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ∈ 𝒫 𝐴)
83, 7sylan2b 493 . . . . 5 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) → ([,]‘𝑤) ∈ 𝒫 𝐴)
98ralrimiva 3068 . . . 4 (𝐴 ∈ (topGen‘ran (,)) → ∀𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴)
10 iccf 12386 . . . . . 6 [,]:(ℝ* × ℝ*)⟶𝒫 ℝ*
11 ffun 6161 . . . . . 6 ([,]:(ℝ* × ℝ*)⟶𝒫 ℝ* → Fun [,])
1210, 11ax-mp 5 . . . . 5 Fun [,]
13 ssrab2 3793 . . . . . . 7 {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)
14 oveq1 6772 . . . . . . . . . . . 12 (𝑥 = 𝑟 → (𝑥 / (2↑𝑦)) = (𝑟 / (2↑𝑦)))
15 oveq1 6772 . . . . . . . . . . . . 13 (𝑥 = 𝑟 → (𝑥 + 1) = (𝑟 + 1))
1615oveq1d 6780 . . . . . . . . . . . 12 (𝑥 = 𝑟 → ((𝑥 + 1) / (2↑𝑦)) = ((𝑟 + 1) / (2↑𝑦)))
1714, 16opeq12d 4517 . . . . . . . . . . 11 (𝑥 = 𝑟 → ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩ = ⟨(𝑟 / (2↑𝑦)), ((𝑟 + 1) / (2↑𝑦))⟩)
18 oveq2 6773 . . . . . . . . . . . . 13 (𝑦 = 𝑠 → (2↑𝑦) = (2↑𝑠))
1918oveq2d 6781 . . . . . . . . . . . 12 (𝑦 = 𝑠 → (𝑟 / (2↑𝑦)) = (𝑟 / (2↑𝑠)))
2018oveq2d 6781 . . . . . . . . . . . 12 (𝑦 = 𝑠 → ((𝑟 + 1) / (2↑𝑦)) = ((𝑟 + 1) / (2↑𝑠)))
2119, 20opeq12d 4517 . . . . . . . . . . 11 (𝑦 = 𝑠 → ⟨(𝑟 / (2↑𝑦)), ((𝑟 + 1) / (2↑𝑦))⟩ = ⟨(𝑟 / (2↑𝑠)), ((𝑟 + 1) / (2↑𝑠))⟩)
2217, 21cbvmpt2v 6852 . . . . . . . . . 10 (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) = (𝑟 ∈ ℤ, 𝑠 ∈ ℕ0 ↦ ⟨(𝑟 / (2↑𝑠)), ((𝑟 + 1) / (2↑𝑠))⟩)
2322dyadf 23480 . . . . . . . . 9 (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ0)⟶( ≤ ∩ (ℝ × ℝ))
24 frn 6166 . . . . . . . . 9 ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) → ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ ( ≤ ∩ (ℝ × ℝ)))
2523, 24ax-mp 5 . . . . . . . 8 ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ ( ≤ ∩ (ℝ × ℝ))
26 inss2 3942 . . . . . . . . 9 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
27 rexpssxrxp 10197 . . . . . . . . 9 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
2826, 27sstri 3718 . . . . . . . 8 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
2925, 28sstri 3718 . . . . . . 7 ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ⊆ (ℝ* × ℝ*)
3013, 29sstri 3718 . . . . . 6 {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ (ℝ* × ℝ*)
3110fdmi 6165 . . . . . 6 dom [,] = (ℝ* × ℝ*)
3230, 31sseqtr4i 3744 . . . . 5 {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]
33 funimass4 6361 . . . . 5 ((Fun [,] ∧ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) → (([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴))
3412, 32, 33mp2an 710 . . . 4 (([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴)
359, 34sylibr 224 . . 3 (𝐴 ∈ (topGen‘ran (,)) → ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴)
36 sspwuni 4719 . . 3 (([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴)
3735, 36sylib 208 . 2 (𝐴 ∈ (topGen‘ran (,)) → ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴)
38 eqid 2724 . . . . . . 7 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
3938rexmet 22716 . . . . . 6 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
40 eqid 2724 . . . . . . . 8 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
4138, 40tgioo 22721 . . . . . . 7 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
4241mopni2 22420 . . . . . 6 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) → ∃𝑟 ∈ ℝ+ (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴)
4339, 42mp3an1 1524 . . . . 5 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) → ∃𝑟 ∈ ℝ+ (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴)
44 elssuni 4575 . . . . . . . . . . 11 (𝐴 ∈ (topGen‘ran (,)) → 𝐴 (topGen‘ran (,)))
45 uniretop 22688 . . . . . . . . . . 11 ℝ = (topGen‘ran (,))
4644, 45syl6sseqr 3758 . . . . . . . . . 10 (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ⊆ ℝ)
4746sselda 3709 . . . . . . . . 9 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) → 𝑤 ∈ ℝ)
48 rpre 11953 . . . . . . . . 9 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
4938bl2ioo 22717 . . . . . . . . 9 ((𝑤 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤𝑟)(,)(𝑤 + 𝑟)))
5047, 48, 49syl2an 495 . . . . . . . 8 (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ 𝑟 ∈ ℝ+) → (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤𝑟)(,)(𝑤 + 𝑟)))
5150sseq1d 3738 . . . . . . 7 (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ 𝑟 ∈ ℝ+) → ((𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 ↔ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴))
52 2re 11203 . . . . . . . . . . 11 2 ∈ ℝ
53 1lt2 11307 . . . . . . . . . . 11 1 < 2
54 expnlbnd 13109 . . . . . . . . . . 11 ((𝑟 ∈ ℝ+ ∧ 2 ∈ ℝ ∧ 1 < 2) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟)
5552, 53, 54mp3an23 1529 . . . . . . . . . 10 (𝑟 ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟)
5655ad2antrl 766 . . . . . . . . 9 (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟)
5747ad2antrr 764 . . . . . . . . . . . 12 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ℝ)
58 2nn 11298 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ
59 nnnn0 11412 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
6059ad2antrl 766 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑛 ∈ ℕ0)
61 nnexpcl 12988 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
6258, 60, 61sylancr 698 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℕ)
6362nnred 11148 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℝ)
6457, 63remulcld 10183 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) ∈ ℝ)
65 fllelt 12713 . . . . . . . . . . . . . . 15 ((𝑤 · (2↑𝑛)) ∈ ℝ → ((⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1)))
6664, 65syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1)))
6766simpld 477 . . . . . . . . . . . . 13 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)))
68 reflcl 12712 . . . . . . . . . . . . . . 15 ((𝑤 · (2↑𝑛)) ∈ ℝ → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ)
6964, 68syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ)
7062nngt0d 11177 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 0 < (2↑𝑛))
71 ledivmul2 11015 . . . . . . . . . . . . . 14 (((⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛))))
7269, 57, 63, 70, 71syl112anc 1443 . . . . . . . . . . . . 13 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛))))
7367, 72mpbird 247 . . . . . . . . . . . 12 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤)
74 peano2re 10322 . . . . . . . . . . . . . . 15 ((⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ)
7569, 74syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ)
7675, 62nndivred 11182 . . . . . . . . . . . . 13 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ∈ ℝ)
7766simprd 482 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1))
78 ltmuldiv 11009 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
7957, 75, 63, 70, 78syl112anc 1443 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
8077, 79mpbid 222 . . . . . . . . . . . . 13 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))
8157, 76, 80ltled 10298 . . . . . . . . . . . 12 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))
8269, 62nndivred 11182 . . . . . . . . . . . . 13 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∈ ℝ)
83 elicc2 12352 . . . . . . . . . . . . 13 ((((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∈ ℝ ∧ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ∈ ℝ) → (𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))))
8482, 76, 83syl2anc 696 . . . . . . . . . . . 12 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))))
8557, 73, 81, 84mpbir3and 1382 . . . . . . . . . . 11 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
8664flcld 12714 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ)
8722dyadval 23481 . . . . . . . . . . . . . 14 (((⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ0) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) = ⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩)
8886, 60, 87syl2anc 696 . . . . . . . . . . . . 13 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) = ⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩)
8988fveq2d 6308 . . . . . . . . . . . 12 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) = ([,]‘⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩))
90 df-ov 6768 . . . . . . . . . . . 12 (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) = ([,]‘⟨((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))⟩)
9189, 90syl6eqr 2776 . . . . . . . . . . 11 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))
9285, 91eleqtrrd 2806 . . . . . . . . . 10 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)))
93 ffn 6158 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩):(ℤ × ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) → (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) Fn (ℤ × ℕ0))
9423, 93ax-mp 5 . . . . . . . . . . . . . 14 (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) Fn (ℤ × ℕ0)
95 fnovrn 6926 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) Fn (ℤ × ℕ0) ∧ (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ0) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩))
9694, 95mp3an1 1524 . . . . . . . . . . . . 13 (((⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ0) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩))
9786, 60, 96syl2anc 696 . . . . . . . . . . . 12 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩))
98 simplrl 819 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ+)
9998rpred 11986 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ)
10057, 99resubcld 10571 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤𝑟) ∈ ℝ)
101100rexrd 10202 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤𝑟) ∈ ℝ*)
10257, 99readdcld 10182 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈ ℝ)
103102rexrd 10202 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈ ℝ*)
10482, 99readdcld 10182 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟) ∈ ℝ)
10569recnd 10181 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℂ)
106 1cnd 10169 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 1 ∈ ℂ)
10763recnd 10181 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℂ)
10862nnne0d 11178 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ≠ 0)
109105, 106, 107, 108divdird 10952 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))))
11062nnrecred 11179 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) ∈ ℝ)
111 simprr 813 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) < 𝑟)
112110, 99, 82, 111ltadd2dd 10309 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))
113109, 112eqbrtrd 4782 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))
11457, 76, 104, 80, 113lttrd 10311 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))
11557, 99, 82ltsubaddd 10736 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟)))
116114, 115mpbird 247 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)))
11757, 110readdcld 10182 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) ∈ ℝ)
11882, 57, 110, 73leadd1dd 10754 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) ≤ (𝑤 + (1 / (2↑𝑛))))
119109, 118eqbrtrd 4782 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ≤ (𝑤 + (1 / (2↑𝑛))))
120110, 99, 57, 111ltadd2dd 10309 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) < (𝑤 + 𝑟))
12176, 117, 102, 119, 120lelttrd 10308 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟))
122 iccssioo 12356 . . . . . . . . . . . . . . 15 ((((𝑤𝑟) ∈ ℝ* ∧ (𝑤 + 𝑟) ∈ ℝ*) ∧ ((𝑤𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∧ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟))) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤𝑟)(,)(𝑤 + 𝑟)))
123101, 103, 116, 121, 122syl22anc 1440 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤𝑟)(,)(𝑤 + 𝑟)))
12491, 123eqsstrd 3745 . . . . . . . . . . . . 13 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ⊆ ((𝑤𝑟)(,)(𝑤 + 𝑟)))
125 simplrr 820 . . . . . . . . . . . . 13 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)
126124, 125sstrd 3719 . . . . . . . . . . . 12 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ⊆ 𝐴)
127 fveq2 6304 . . . . . . . . . . . . . 14 (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) → ([,]‘𝑧) = ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)))
128127sseq1d 3738 . . . . . . . . . . . . 13 (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ⊆ 𝐴))
129128elrab 3469 . . . . . . . . . . . 12 (((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ↔ (((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∧ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ⊆ 𝐴))
13097, 126, 129sylanbrc 701 . . . . . . . . . . 11 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})
131 funfvima2 6608 . . . . . . . . . . . 12 ((Fun [,] ∧ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) → (((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})))
13212, 32, 131mp2an 710 . . . . . . . . . . 11 (((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
133130, 132syl 17 . . . . . . . . . 10 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
134 elunii 4549 . . . . . . . . . 10 ((𝑤 ∈ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∧ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})) → 𝑤 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
13592, 133, 134syl2anc 696 . . . . . . . . 9 ((((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
13656, 135rexlimddv 3137 . . . . . . . 8 (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → 𝑤 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
137136expr 644 . . . . . . 7 (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ 𝑟 ∈ ℝ+) → (((𝑤𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴𝑤 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})))
13851, 137sylbid 230 . . . . . 6 (((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) ∧ 𝑟 ∈ ℝ+) → ((𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴𝑤 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})))
139138rexlimdva 3133 . . . . 5 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) → (∃𝑟 ∈ ℝ+ (𝑤(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴𝑤 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})))
14043, 139mpd 15 . . . 4 ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤𝐴) → 𝑤 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
141140ex 449 . . 3 (𝐴 ∈ (topGen‘ran (,)) → (𝑤𝐴𝑤 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴})))
142141ssrdv 3715 . 2 (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}))
14337, 142eqssd 3726 1 (𝐴 ∈ (topGen‘ran (,)) → ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1596   ∈ wcel 2103  ∀wral 3014  ∃wrex 3015  {crab 3018   ∩ cin 3679   ⊆ wss 3680  𝒫 cpw 4266  ⟨cop 4291  ∪ cuni 4544   class class class wbr 4760   × cxp 5216  dom cdm 5218  ran crn 5219   ↾ cres 5220   “ cima 5221   ∘ ccom 5222  Fun wfun 5995   Fn wfn 5996  ⟶wf 5997  ‘cfv 6001  (class class class)co 6765   ↦ cmpt2 6767  ℝcr 10048  0cc0 10049  1c1 10050   + caddc 10052   · cmul 10054  ℝ*cxr 10186   < clt 10187   ≤ cle 10188   − cmin 10379   / cdiv 10797  ℕcn 11133  2c2 11183  ℕ0cn0 11405  ℤcz 11490  ℝ+crp 11946  (,)cioo 12289  [,]cicc 12292  ⌊cfl 12706  ↑cexp 12975  abscabs 14094  topGenctg 16221  ∞Metcxmt 19854  ballcbl 19856  MetOpencmopn 19859 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-er 7862  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-sup 8464  df-inf 8465  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-n0 11406  df-z 11491  df-uz 11801  df-q 11903  df-rp 11947  df-xneg 12060  df-xadd 12061  df-xmul 12062  df-ioo 12293  df-icc 12296  df-fl 12708  df-seq 12917  df-exp 12976  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-topgen 16227  df-psmet 19861  df-xmet 19862  df-met 19863  df-bl 19864  df-mopn 19865  df-top 20822  df-topon 20839  df-bases 20873 This theorem is referenced by:  mblfinlem1  33678  mblfinlem2  33679
 Copyright terms: Public domain W3C validator