This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscfil3

Description: A filter is Cauchy iff it contains a ball of any chosen size. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion iscfil3 ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) ) )

Proof

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 ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ) ) )