Metamath Proof Explorer


Theorem metustel

Description: Define a filter base F generated by a metric D . (Contributed by Thierry Arnoux, 22-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metust.1 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
Assertion metustel ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵𝐹 ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )

Proof

Step Hyp Ref Expression
1 metust.1 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
2 1 eleq2i ( 𝐵𝐹𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
3 elex ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝐵 ∈ V )
4 3 a1i ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝐵 ∈ V ) )
5 cnvexg ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 ∈ V )
6 imaexg ( 𝐷 ∈ V → ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ V )
7 eleq1a ( ( 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ V → ( 𝐵 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝐵 ∈ V ) )
8 5 6 7 3syl ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝐵 ∈ V ) )
9 8 rexlimdvw ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ∃ 𝑎 ∈ ℝ+ 𝐵 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝐵 ∈ V ) )
10 eqid ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) )
11 10 elrnmpt ( 𝐵 ∈ V → ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
12 11 a1i ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 ∈ V → ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )
13 4 9 12 pm5.21ndd ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
14 2 13 syl5bb ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵𝐹 ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) )