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

Metamath Proof Explorer

Theorem metustfbas

Description: The filter base generated by a metric D . (Contributed by Thierry Arnoux, 26-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Hypothesis metust.1 ⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
Assertion metustfbas ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 metust.1 ⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
2 1 metustel ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ+ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
3 simpr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
4 cnvimass ⊢ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ dom 𝐷
5 psmetf ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
6 5 fdmd ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
7 6 adantr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
8 4 7 sseqtrid ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( 𝑋 × 𝑋 ) )
9 3 8 eqsstrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝑥 ⊆ ( 𝑋 × 𝑋 ) )
10 9 ex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝑥 ⊆ ( 𝑋 × 𝑋 ) ) )
11 10 rexlimdvw ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ∃ 𝑎 ∈ ℝ+ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝑥 ⊆ ( 𝑋 × 𝑋 ) ) )
12 2 11 sylbid ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ⊆ ( 𝑋 × 𝑋 ) ) )
13 12 ralrimiv ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑋 × 𝑋 ) )
14 pwssb ⊢ ( 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ↔ ∀ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑋 × 𝑋 ) )
15 13 14 sylibr ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
16 15 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
17 cnvexg ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ◡ 𝐷 ∈ V )
18 imaexg ⊢ ( ◡ 𝐷 ∈ V → ( ◡ 𝐷 “ ( 0 [,) 1 ) ) ∈ V )
19 elisset ⊢ ( ( ◡ 𝐷 “ ( 0 [,) 1 ) ) ∈ V → ∃ 𝑥 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 1 ) ) )
20 1rp ⊢ 1 ∈ ℝ+
21 oveq2 ⊢ ( 𝑎 = 1 → ( 0 [,) 𝑎 ) = ( 0 [,) 1 ) )
22 21 imaeq2d ⊢ ( 𝑎 = 1 → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) = ( ◡ 𝐷 “ ( 0 [,) 1 ) ) )
23 22 rspceeqv ⊢ ( ( 1 ∈ ℝ+ ∧ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 1 ) ) ) → ∃ 𝑎 ∈ ℝ+ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
24 20 23 mpan ⊢ ( 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 1 ) ) → ∃ 𝑎 ∈ ℝ+ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
25 24 eximi ⊢ ( ∃ 𝑥 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 1 ) ) → ∃ 𝑥 ∃ 𝑎 ∈ ℝ+ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
26 17 18 19 25 4syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∃ 𝑥 ∃ 𝑎 ∈ ℝ+ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
27 2 exbidv ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ∃ 𝑥 𝑥 ∈ 𝐹 ↔ ∃ 𝑥 ∃ 𝑎 ∈ ℝ+ 𝑥 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
28 26 27 mpbird ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∃ 𝑥 𝑥 ∈ 𝐹 )
29 28 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∃ 𝑥 𝑥 ∈ 𝐹 )
30 n0 ⊢ ( 𝐹 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐹 )
31 29 30 sylibr ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ≠ ∅ )
32 1 metustid ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) → ( I ↾ 𝑋 ) ⊆ 𝑥 )
33 32 adantll ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( I ↾ 𝑋 ) ⊆ 𝑥 )
34 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ 𝑋 )
35 34 biimpi ⊢ ( 𝑋 ≠ ∅ → ∃ 𝑝 𝑝 ∈ 𝑋 )
36 35 adantr ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∃ 𝑝 𝑝 ∈ 𝑋 )
37 opelidres ⊢ ( 𝑝 ∈ 𝑋 → ( ⟨ 𝑝 , 𝑝 ⟩ ∈ ( I ↾ 𝑋 ) ↔ 𝑝 ∈ 𝑋 ) )
38 37 ibir ⊢ ( 𝑝 ∈ 𝑋 → ⟨ 𝑝 , 𝑝 ⟩ ∈ ( I ↾ 𝑋 ) )
39 38 ne0d ⊢ ( 𝑝 ∈ 𝑋 → ( I ↾ 𝑋 ) ≠ ∅ )
40 39 exlimiv ⊢ ( ∃ 𝑝 𝑝 ∈ 𝑋 → ( I ↾ 𝑋 ) ≠ ∅ )
41 36 40 syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( I ↾ 𝑋 ) ≠ ∅ )
42 41 adantr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( I ↾ 𝑋 ) ≠ ∅ )
43 ssn0 ⊢ ( ( ( I ↾ 𝑋 ) ⊆ 𝑥 ∧ ( I ↾ 𝑋 ) ≠ ∅ ) → 𝑥 ≠ ∅ )
44 33 42 43 syl2anc ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ≠ ∅ )
45 44 nelrdva ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ¬ ∅ ∈ 𝐹 )
46 df-nel ⊢ ( ∅ ∉ 𝐹 ↔ ¬ ∅ ∈ 𝐹 )
47 45 46 sylibr ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∅ ∉ 𝐹 )
48 dfss2 ⊢ ( 𝑥 ⊆ 𝑦 ↔ ( 𝑥 ∩ 𝑦 ) = 𝑥 )
49 48 biimpi ⊢ ( 𝑥 ⊆ 𝑦 → ( 𝑥 ∩ 𝑦 ) = 𝑥 )
50 49 adantl ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∩ 𝑦 ) = 𝑥 )
51 simplrl ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑥 ⊆ 𝑦 ) → 𝑥 ∈ 𝐹 )
52 50 51 eqeltrd ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
53 sseqin2 ⊢ ( 𝑦 ⊆ 𝑥 ↔ ( 𝑥 ∩ 𝑦 ) = 𝑦 )
54 53 biimpi ⊢ ( 𝑦 ⊆ 𝑥 → ( 𝑥 ∩ 𝑦 ) = 𝑦 )
55 54 adantl ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑦 ⊆ 𝑥 ) → ( 𝑥 ∩ 𝑦 ) = 𝑦 )
56 simplrr ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ∈ 𝐹 )
57 55 56 eqeltrd ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ∧ 𝑦 ⊆ 𝑥 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
58 simplr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
59 simprl ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → 𝑥 ∈ 𝐹 )
60 simprr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → 𝑦 ∈ 𝐹 )
61 1 metustto ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )
62 58 59 60 61 syl3anc ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 ) )
63 52 57 62 mpjaodan ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
64 ssidd ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) )
65 sseq1 ⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
66 65 rspcev ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
67 63 64 66 syl2anc ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
68 67 ralrimivva ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
69 31 47 68 3jca ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
70 elfvex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
71 70 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝑋 ∈ V )
72 71 71 xpexd ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑋 × 𝑋 ) ∈ V )
73 isfbas2 ⊢ ( ( 𝑋 × 𝑋 ) ∈ V → ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
74 72 73 syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
75 16 69 74 mpbir2and ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )