Metamath Proof Explorer


Theorem cfilucfil

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil . (Contributed by Thierry Arnoux, 29-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metust.1 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
Assertion cfilucfil ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 metust.1 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
2 1 metust ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) )
3 cfilufbas ( ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
4 2 3 sylan ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
5 simpllr ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
6 psmetf ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
7 ffun ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → Fun 𝐷 )
8 5 6 7 3syl ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → Fun 𝐷 )
9 2 ad2antrr ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) )
10 simplr ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) )
11 1 metustfbas ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
12 11 ad2antrr ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
13 cnvimass ( 𝐷 “ ( 0 [,) 𝑥 ) ) ⊆ dom 𝐷
14 fdm ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → dom 𝐷 = ( 𝑋 × 𝑋 ) )
15 5 6 14 3syl ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
16 13 15 sseqtrid ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐷 “ ( 0 [,) 𝑥 ) ) ⊆ ( 𝑋 × 𝑋 ) )
17 simpr ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
18 17 rphalfcld ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ+ )
19 eqidd ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) )
20 oveq2 ( 𝑎 = ( 𝑥 / 2 ) → ( 0 [,) 𝑎 ) = ( 0 [,) ( 𝑥 / 2 ) ) )
21 20 imaeq2d ( 𝑎 = ( 𝑥 / 2 ) → ( 𝐷 “ ( 0 [,) 𝑎 ) ) = ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) )
22 21 rspceeqv ( ( ( 𝑥 / 2 ) ∈ ℝ+ ∧ ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ) → ∃ 𝑎 ∈ ℝ+ ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
23 18 19 22 syl2anc ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ+ ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
24 1 metustel ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ+ ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
25 24 biimpar ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ∃ 𝑎 ∈ ℝ+ ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ∈ 𝐹 )
26 5 23 25 syl2anc ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ∈ 𝐹 )
27 0xr 0 ∈ ℝ*
28 27 a1i ( 𝑥 ∈ ℝ+ → 0 ∈ ℝ* )
29 rpxr ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ* )
30 0le0 0 ≤ 0
31 30 a1i ( 𝑥 ∈ ℝ+ → 0 ≤ 0 )
32 rpre ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ )
33 32 rehalfcld ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ )
34 rphalflt ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) < 𝑥 )
35 33 32 34 ltled ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ≤ 𝑥 )
36 icossico ( ( ( 0 ∈ ℝ*𝑥 ∈ ℝ* ) ∧ ( 0 ≤ 0 ∧ ( 𝑥 / 2 ) ≤ 𝑥 ) ) → ( 0 [,) ( 𝑥 / 2 ) ) ⊆ ( 0 [,) 𝑥 ) )
37 28 29 31 35 36 syl22anc ( 𝑥 ∈ ℝ+ → ( 0 [,) ( 𝑥 / 2 ) ) ⊆ ( 0 [,) 𝑥 ) )
38 imass2 ( ( 0 [,) ( 𝑥 / 2 ) ) ⊆ ( 0 [,) 𝑥 ) → ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) )
39 17 37 38 3syl ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) )
40 sseq1 ( 𝑤 = ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) → ( 𝑤 ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) ↔ ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) ) )
41 40 rspcev ( ( ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ∈ 𝐹 ∧ ( 𝐷 “ ( 0 [,) ( 𝑥 / 2 ) ) ) ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) ) → ∃ 𝑤𝐹 𝑤 ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) )
42 26 39 41 syl2anc ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑤𝐹 𝑤 ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) )
43 elfg ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ( ( 𝐷 “ ( 0 [,) 𝑥 ) ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ↔ ( ( 𝐷 “ ( 0 [,) 𝑥 ) ) ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤𝐹 𝑤 ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) ) ) )
44 43 biimpar ( ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝐷 “ ( 0 [,) 𝑥 ) ) ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤𝐹 𝑤 ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) ) ) → ( 𝐷 “ ( 0 [,) 𝑥 ) ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
45 12 16 42 44 syl12anc ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐷 “ ( 0 [,) 𝑥 ) ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
46 cfiluexsm ( ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ ( 𝐷 “ ( 0 [,) 𝑥 ) ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) )
47 9 10 45 46 syl3anc ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) )
48 funimass2 ( ( Fun 𝐷 ∧ ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) ) → ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
49 48 ex ( Fun 𝐷 → ( ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) → ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
50 49 reximdv ( Fun 𝐷 → ( ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑥 ) ) → ∃ 𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
51 8 47 50 sylc ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
52 51 ralrimiva ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) → ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
53 4 52 jca ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ) → ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
54 simprl ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
55 oveq2 ( 𝑥 = 𝑎 → ( 0 [,) 𝑥 ) = ( 0 [,) 𝑎 ) )
56 55 sseq2d ( 𝑥 = 𝑎 → ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ) )
57 56 rexbidv ( 𝑥 = 𝑎 → ( ∃ 𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∃ 𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ) )
58 simp-4r ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
59 58 simprd ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
60 simplr ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → 𝑎 ∈ ℝ+ )
61 57 59 60 rspcdva ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) )
62 nfv 𝑦 ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
63 nfv 𝑦 𝐶 ∈ ( fBas ‘ 𝑋 )
64 nfcv 𝑦+
65 nfre1 𝑦𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 )
66 64 65 nfralw 𝑦𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 )
67 63 66 nfan 𝑦 ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
68 62 67 nfan 𝑦 ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
69 nfv 𝑦 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 )
70 68 69 nfan 𝑦 ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
71 nfv 𝑦 𝑎 ∈ ℝ+
72 70 71 nfan 𝑦 ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ )
73 nfv 𝑦 ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣
74 72 73 nfan 𝑦 ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
75 54 ad4antr ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦𝐶 ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
76 fbelss ( ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦𝐶 ) → 𝑦𝑋 )
77 75 76 sylancom ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦𝐶 ) → 𝑦𝑋 )
78 xpss12 ( ( 𝑦𝑋𝑦𝑋 ) → ( 𝑦 × 𝑦 ) ⊆ ( 𝑋 × 𝑋 ) )
79 77 77 78 syl2anc ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦𝐶 ) → ( 𝑦 × 𝑦 ) ⊆ ( 𝑋 × 𝑋 ) )
80 simp-6r ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦𝐶 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
81 80 6 14 3syl ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦𝐶 ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
82 79 81 sseqtrrd ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ∧ 𝑦𝐶 ) → ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 )
83 82 ex ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ( 𝑦𝐶 → ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) )
84 74 83 ralrimi ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∀ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 )
85 r19.29r ( ( ∃ 𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ∀ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ∃ 𝑦𝐶 ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) )
86 sseqin2 ( ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ↔ ( dom 𝐷 ∩ ( 𝑦 × 𝑦 ) ) = ( 𝑦 × 𝑦 ) )
87 86 biimpi ( ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 → ( dom 𝐷 ∩ ( 𝑦 × 𝑦 ) ) = ( 𝑦 × 𝑦 ) )
88 87 adantl ( ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ( dom 𝐷 ∩ ( 𝑦 × 𝑦 ) ) = ( 𝑦 × 𝑦 ) )
89 dminss ( dom 𝐷 ∩ ( 𝑦 × 𝑦 ) ) ⊆ ( 𝐷 “ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) )
90 88 89 eqsstrrdi ( ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ) )
91 imass2 ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) → ( 𝐷 “ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
92 91 adantr ( ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ( 𝐷 “ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
93 90 92 sstrd ( ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
94 93 reximi ( ∃ 𝑦𝐶 ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
95 85 94 syl ( ( ∃ 𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑎 ) ∧ ∀ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
96 61 84 95 syl2anc ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
97 r19.41v ( ∃ 𝑦𝐶 ( ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) ↔ ( ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) )
98 sstr ( ( ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
99 98 reximi ( ∃ 𝑦𝐶 ( ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
100 97 99 sylbir ( ( ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
101 96 100 sylancom ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
102 simp-5r ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤𝐹 ) ∧ 𝑤𝑣 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
103 simplr ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤𝐹 ) ∧ 𝑤𝑣 ) → 𝑤𝐹 )
104 1 metustel ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑤𝐹 ↔ ∃ 𝑎 ∈ ℝ+ 𝑤 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
105 104 biimpa ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑤𝐹 ) → ∃ 𝑎 ∈ ℝ+ 𝑤 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
106 102 103 105 syl2anc ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤𝐹 ) ∧ 𝑤𝑣 ) → ∃ 𝑎 ∈ ℝ+ 𝑤 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
107 r19.41v ( ∃ 𝑎 ∈ ℝ+ ( 𝑤 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤𝑣 ) ↔ ( ∃ 𝑎 ∈ ℝ+ 𝑤 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤𝑣 ) )
108 sseq1 ( 𝑤 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) → ( 𝑤𝑣 ↔ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 ) )
109 108 biimpa ( ( 𝑤 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤𝑣 ) → ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
110 109 reximi ( ∃ 𝑎 ∈ ℝ+ ( 𝑤 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤𝑣 ) → ∃ 𝑎 ∈ ℝ+ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
111 107 110 sylbir ( ( ∃ 𝑎 ∈ ℝ+ 𝑤 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∧ 𝑤𝑣 ) → ∃ 𝑎 ∈ ℝ+ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
112 106 111 sylancom ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤𝐹 ) ∧ 𝑤𝑣 ) → ∃ 𝑎 ∈ ℝ+ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
113 11 ad2antrr ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
114 elfg ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ( 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ↔ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤𝐹 𝑤𝑣 ) ) )
115 114 biimpa ( ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤𝐹 𝑤𝑣 ) )
116 113 115 sylancom ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤𝐹 𝑤𝑣 ) )
117 116 simprd ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑤𝐹 𝑤𝑣 )
118 112 117 r19.29a ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑎 ∈ ℝ+ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ 𝑣 )
119 101 118 r19.29a ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
120 119 ralrimiva ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → ∀ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 )
121 2 adantr ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) )
122 iscfilu ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 ) ) )
123 121 122 syl ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → ( 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∃ 𝑦𝐶 ( 𝑦 × 𝑦 ) ⊆ 𝑣 ) ) )
124 54 120 123 mpbir2and ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) )
125 53 124 impbida ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )