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	bitrid	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )