| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cfilfil |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
| 2 |
|
cfil3i |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) |
| 3 |
2
|
3expa |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) |
| 4 |
3
|
ralrimiva |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) |
| 5 |
1 4
|
jca |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) ) |
| 6 |
|
simprl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
| 7 |
|
rphalfcl |
⊢ ( 𝑠 ∈ ℝ+ → ( 𝑠 / 2 ) ∈ ℝ+ ) |
| 8 |
7
|
adantl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) → ( 𝑠 / 2 ) ∈ ℝ+ ) |
| 9 |
|
oveq2 |
⊢ ( 𝑟 = ( 𝑠 / 2 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) |
| 10 |
9
|
eleq1d |
⊢ ( 𝑟 = ( 𝑠 / 2 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ↔ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) |
| 11 |
10
|
rexbidv |
⊢ ( 𝑟 = ( 𝑠 / 2 ) → ( ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) |
| 12 |
11
|
rspcv |
⊢ ( ( 𝑠 / 2 ) ∈ ℝ+ → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) |
| 13 |
8 12
|
syl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) |
| 14 |
|
simprr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) |
| 15 |
|
simp-4l |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 16 |
|
simplrl |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝑥 ∈ 𝑋 ) |
| 17 |
|
simpllr |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝑠 ∈ ℝ+ ) |
| 18 |
17
|
rpred |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝑠 ∈ ℝ ) |
| 19 |
|
simprl |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) |
| 20 |
|
blhalf |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑠 ∈ ℝ ∧ 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ⊆ ( 𝑢 ( ball ‘ 𝐷 ) 𝑠 ) ) |
| 21 |
15 16 18 19 20
|
syl22anc |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ⊆ ( 𝑢 ( ball ‘ 𝐷 ) 𝑠 ) ) |
| 22 |
|
simprr |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) |
| 23 |
21 22
|
sseldd |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝑣 ∈ ( 𝑢 ( ball ‘ 𝐷 ) 𝑠 ) ) |
| 24 |
17
|
rpxrd |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝑠 ∈ ℝ* ) |
| 25 |
17 7
|
syl |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → ( 𝑠 / 2 ) ∈ ℝ+ ) |
| 26 |
25
|
rpxrd |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → ( 𝑠 / 2 ) ∈ ℝ* ) |
| 27 |
|
blssm |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑠 / 2 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ⊆ 𝑋 ) |
| 28 |
15 16 26 27
|
syl3anc |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ⊆ 𝑋 ) |
| 29 |
28 19
|
sseldd |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝑢 ∈ 𝑋 ) |
| 30 |
28 22
|
sseldd |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → 𝑣 ∈ 𝑋 ) |
| 31 |
|
elbl2 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑠 ∈ ℝ* ) ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ( 𝑣 ∈ ( 𝑢 ( ball ‘ 𝐷 ) 𝑠 ) ↔ ( 𝑢 𝐷 𝑣 ) < 𝑠 ) ) |
| 32 |
15 24 29 30 31
|
syl22anc |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → ( 𝑣 ∈ ( 𝑢 ( ball ‘ 𝐷 ) 𝑠 ) ↔ ( 𝑢 𝐷 𝑣 ) < 𝑠 ) ) |
| 33 |
23 32
|
mpbid |
⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∧ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ) ) → ( 𝑢 𝐷 𝑣 ) < 𝑠 ) |
| 34 |
33
|
ralrimivva |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) → ∀ 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∀ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ( 𝑢 𝐷 𝑣 ) < 𝑠 ) |
| 35 |
|
raleq |
⊢ ( 𝑦 = ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) → ( ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ↔ ∀ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ( 𝑢 𝐷 𝑣 ) < 𝑠 ) ) |
| 36 |
35
|
raleqbi1dv |
⊢ ( 𝑦 = ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) → ( ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ↔ ∀ 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∀ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ( 𝑢 𝐷 𝑣 ) < 𝑠 ) ) |
| 37 |
36
|
rspcev |
⊢ ( ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ∧ ∀ 𝑢 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∀ 𝑣 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ( 𝑢 𝐷 𝑣 ) < 𝑠 ) → ∃ 𝑦 ∈ 𝐹 ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ) |
| 38 |
14 34 37
|
syl2anc |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 ) ) → ∃ 𝑦 ∈ 𝐹 ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ) |
| 39 |
38
|
rexlimdvaa |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) → ( ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑠 / 2 ) ) ∈ 𝐹 → ∃ 𝑦 ∈ 𝐹 ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ) ) |
| 40 |
13 39
|
syld |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ ℝ+ ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 → ∃ 𝑦 ∈ 𝐹 ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ) ) |
| 41 |
40
|
ralrimdva |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 → ∀ 𝑠 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ) ) |
| 42 |
41
|
impr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) ) → ∀ 𝑠 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ) |
| 43 |
|
iscfil2 |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ) ) ) |
| 44 |
43
|
adantr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 𝐷 𝑣 ) < 𝑠 ) ) ) |
| 45 |
6 42 44
|
mpbir2and |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) ) → 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) |
| 46 |
5 45
|
impbida |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) ) ) |