Step |
Hyp |
Ref |
Expression |
1 |
|
lebnum.j |
⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) |
2 |
|
lebnum.d |
⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
3 |
|
lebnum.c |
⊢ ( 𝜑 → 𝐽 ∈ Comp ) |
4 |
|
lebnum.s |
⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 ) |
5 |
|
lebnum.u |
⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 ) |
6 |
|
metxmet |
⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
7 |
2 6
|
syl |
⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
8 |
1
|
mopnuni |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
9 |
7 8
|
syl |
⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 ) |
10 |
9 5
|
eqtr3d |
⊢ ( 𝜑 → ∪ 𝐽 = ∪ 𝑈 ) |
11 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
12 |
11
|
cmpcov |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) → ∃ 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∪ 𝐽 = ∪ 𝑤 ) |
13 |
3 4 10 12
|
syl3anc |
⊢ ( 𝜑 → ∃ 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∪ 𝐽 = ∪ 𝑤 ) |
14 |
|
1rp |
⊢ 1 ∈ ℝ+ |
15 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ) |
16 |
15
|
elin1d |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → 𝑤 ∈ 𝒫 𝑈 ) |
17 |
16
|
elpwid |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → 𝑤 ⊆ 𝑈 ) |
18 |
17
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑤 ⊆ 𝑈 ) |
19 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ 𝑤 ) |
20 |
18 19
|
sseldd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ 𝑈 ) |
21 |
7
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
22 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 ) |
23 |
|
rpxr |
⊢ ( 1 ∈ ℝ+ → 1 ∈ ℝ* ) |
24 |
14 23
|
mp1i |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 1 ∈ ℝ* ) |
25 |
|
blssm |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 1 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 ) |
26 |
21 22 24 25
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 ) |
27 |
|
sseq2 |
⊢ ( 𝑢 = 𝑋 → ( ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ↔ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 ) ) |
28 |
27
|
rspcev |
⊢ ( ( 𝑋 ∈ 𝑈 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) |
29 |
20 26 28
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) |
30 |
29
|
ralrimiva |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) |
31 |
|
oveq2 |
⊢ ( 𝑑 = 1 → ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) = ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) |
32 |
31
|
sseq1d |
⊢ ( 𝑑 = 1 → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) ) |
33 |
32
|
rexbidv |
⊢ ( 𝑑 = 1 → ( ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) ) |
34 |
33
|
ralbidv |
⊢ ( 𝑑 = 1 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) ) |
35 |
34
|
rspcev |
⊢ ( ( 1 ∈ ℝ+ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) |
36 |
14 30 35
|
sylancr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) |
37 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
38 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝐽 ∈ Comp ) |
39 |
17
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑤 ⊆ 𝑈 ) |
40 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑈 ⊆ 𝐽 ) |
41 |
39 40
|
sstrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑤 ⊆ 𝐽 ) |
42 |
9
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑋 = ∪ 𝐽 ) |
43 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ∪ 𝐽 = ∪ 𝑤 ) |
44 |
42 43
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑋 = ∪ 𝑤 ) |
45 |
15
|
elin2d |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → 𝑤 ∈ Fin ) |
46 |
45
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑤 ∈ Fin ) |
47 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ¬ 𝑋 ∈ 𝑤 ) |
48 |
|
eqid |
⊢ ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ* , < ) ) |
49 |
|
eqid |
⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) |
50 |
1 37 38 41 44 46 47 48 49
|
lebnumlem3 |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) |
51 |
|
ssrexv |
⊢ ( 𝑤 ⊆ 𝑈 → ( ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 → ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) ) |
52 |
39 51
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ( ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 → ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) ) |
53 |
52
|
ralimdv |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) ) |
54 |
53
|
reximdv |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) ) |
55 |
50 54
|
mpd |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) |
56 |
36 55
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) |
57 |
13 56
|
rexlimddv |
⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) |