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

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 [,) 𝑥 ) ) ) )