Step | Hyp | Ref
| Expression |
1 | | bcth.2 |
. . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) |
2 | | simpll 790 |
. . . . . 6
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽)) ∧ ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) → 𝐷 ∈ (CMet‘𝑋)) |
3 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋)) |
4 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑚 → (𝑟 ∈ ℝ+ ↔ 𝑚 ∈
ℝ+)) |
5 | 3, 4 | bi2anan9 917 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑦 ∧ 𝑟 = 𝑚) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ↔ (𝑦 ∈ 𝑋 ∧ 𝑚 ∈
ℝ+))) |
6 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑦 ∧ 𝑟 = 𝑚) → 𝑟 = 𝑚) |
7 | 6 | breq1d 4663 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑦 ∧ 𝑟 = 𝑚) → (𝑟 < (1 / 𝑘) ↔ 𝑚 < (1 / 𝑘))) |
8 | | oveq12 6659 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑦 ∧ 𝑟 = 𝑚) → (𝑥(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)𝑚)) |
9 | 8 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑦 ∧ 𝑟 = 𝑚) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) = ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚))) |
10 | 9 | sseq1d 3632 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑦 ∧ 𝑟 = 𝑚) → (((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ↔ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) |
11 | 7, 10 | anbi12d 747 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑦 ∧ 𝑟 = 𝑚) → ((𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) ↔ (𝑚 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))) |
12 | 5, 11 | anbi12d 747 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑦 ∧ 𝑟 = 𝑚) → (((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) ↔ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
13 | 12 | cbvopabv 4722 |
. . . . . . . 8
⊢
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} = {〈𝑦, 𝑚〉 ∣ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} |
14 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (1 / 𝑘) = (1 / 𝑛)) |
15 | 14 | breq2d 4665 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → (𝑚 < (1 / 𝑘) ↔ 𝑚 < (1 / 𝑛))) |
16 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝑀‘𝑘) = (𝑀‘𝑛)) |
17 | 16 | difeq2d 3728 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) = (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛))) |
18 | 17 | sseq2d 3633 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → (((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ↔ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛)))) |
19 | 15, 18 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → ((𝑚 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) ↔ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛))))) |
20 | 19 | anbi2d 740 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) ↔ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛)))))) |
21 | 20 | opabbidv 4716 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → {〈𝑦, 𝑚〉 ∣ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} = {〈𝑦, 𝑚〉 ∣ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛))))}) |
22 | 13, 21 | syl5eq 2668 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} = {〈𝑦, 𝑚〉 ∣ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛))))}) |
23 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑔 → ((ball‘𝐷)‘𝑧) = ((ball‘𝐷)‘𝑔)) |
24 | 23 | difeq1d 3727 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑔 → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛)) = (((ball‘𝐷)‘𝑔) ∖ (𝑀‘𝑛))) |
25 | 24 | sseq2d 3633 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑔 → (((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛)) ↔ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑔) ∖ (𝑀‘𝑛)))) |
26 | 25 | anbi2d 740 |
. . . . . . . . 9
⊢ (𝑧 = 𝑔 → ((𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛))) ↔ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑔) ∖ (𝑀‘𝑛))))) |
27 | 26 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑧 = 𝑔 → (((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛)))) ↔ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑔) ∖ (𝑀‘𝑛)))))) |
28 | 27 | opabbidv 4716 |
. . . . . . 7
⊢ (𝑧 = 𝑔 → {〈𝑦, 𝑚〉 ∣ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑛))))} = {〈𝑦, 𝑚〉 ∣ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑔) ∖ (𝑀‘𝑛))))}) |
29 | 22, 28 | cbvmpt2v 6735 |
. . . . . 6
⊢ (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))}) = (𝑛 ∈ ℕ, 𝑔 ∈ (𝑋 × ℝ+) ↦
{〈𝑦, 𝑚〉 ∣ ((𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) ∧ (𝑚 < (1 / 𝑛) ∧ ((cls‘𝐽)‘(𝑦(ball‘𝐷)𝑚)) ⊆ (((ball‘𝐷)‘𝑔) ∖ (𝑀‘𝑛))))}) |
30 | | simplr 792 |
. . . . . 6
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽)) ∧ ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) → 𝑀:ℕ⟶(Clsd‘𝐽)) |
31 | | simpr 477 |
. . . . . . 7
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽)) ∧ ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) → ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) |
32 | 16 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((int‘𝐽)‘(𝑀‘𝑘)) = ((int‘𝐽)‘(𝑀‘𝑛))) |
33 | 32 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (((int‘𝐽)‘(𝑀‘𝑘)) = ∅ ↔ ((int‘𝐽)‘(𝑀‘𝑛)) = ∅)) |
34 | 33 | cbvralv 3171 |
. . . . . . 7
⊢
(∀𝑘 ∈
ℕ ((int‘𝐽)‘(𝑀‘𝑘)) = ∅ ↔ ∀𝑛 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑛)) = ∅) |
35 | 31, 34 | sylib 208 |
. . . . . 6
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽)) ∧ ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) → ∀𝑛 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑛)) = ∅) |
36 | 1, 2, 29, 30, 35 | bcthlem5 23125 |
. . . . 5
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽)) ∧ ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) → ((int‘𝐽)‘∪ ran 𝑀) = ∅) |
37 | 36 | ex 450 |
. . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽)) → (∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅ → ((int‘𝐽)‘∪ ran 𝑀) = ∅)) |
38 | 37 | necon3ad 2807 |
. . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽)) → (((int‘𝐽)‘∪ ran 𝑀) ≠ ∅ → ¬ ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅)) |
39 | 38 | 3impia 1261 |
. 2
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽) ∧ ((int‘𝐽)‘∪ ran 𝑀) ≠ ∅) → ¬ ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) |
40 | | df-ne 2795 |
. . . 4
⊢
(((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅ ↔ ¬
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) |
41 | 40 | rexbii 3041 |
. . 3
⊢
(∃𝑘 ∈
ℕ ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅ ↔ ∃𝑘 ∈ ℕ ¬
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) |
42 | | rexnal 2995 |
. . 3
⊢
(∃𝑘 ∈
ℕ ¬ ((int‘𝐽)‘(𝑀‘𝑘)) = ∅ ↔ ¬ ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) |
43 | 41, 42 | bitri 264 |
. 2
⊢
(∃𝑘 ∈
ℕ ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅ ↔ ¬ ∀𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) |
44 | 39, 43 | sylibr 224 |
1
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽) ∧ ((int‘𝐽)‘∪ ran 𝑀) ≠ ∅) → ∃𝑘 ∈ ℕ
((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅) |