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

Metamath Proof Explorer

Theorem metustss

Description: Range of the elements of the filter base generated by the metric D . (Contributed by Thierry Arnoux, 28-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

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

Proof

Step Hyp Ref Expression
1 metust.1 ⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
2 cnvimass ⊢ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ dom 𝐷
3 psmetf ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
4 2 3 fssdm ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( 𝑋 × 𝑋 ) )
5 4 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ+ ) → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( 𝑋 × 𝑋 ) )
6 cnvexg ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ◡ 𝐷 ∈ V )
7 imaexg ⊢ ( ◡ 𝐷 ∈ V → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ V )
8 elpwg ⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ V → ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ 𝒫 ( 𝑋 × 𝑋 ) ↔ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( 𝑋 × 𝑋 ) ) )
9 6 7 8 3syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ 𝒫 ( 𝑋 × 𝑋 ) ↔ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( 𝑋 × 𝑋 ) ) )
10 9 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ+ ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ 𝒫 ( 𝑋 × 𝑋 ) ↔ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ⊆ ( 𝑋 × 𝑋 ) ) )
11 5 10 mpbird ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ+ ) → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ 𝒫 ( 𝑋 × 𝑋 ) )
12 11 ralrimiva ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ∀ 𝑎 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ 𝒫 ( 𝑋 × 𝑋 ) )
13 eqid ⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
14 13 rnmptss ⊢ ( ∀ 𝑎 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ 𝒫 ( 𝑋 × 𝑋 ) → ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
15 12 14 syl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
16 1 15 eqsstrid ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐹 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
17 simpr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ∈ 𝐹 )
18 16 17 sseldd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ∈ 𝒫 ( 𝑋 × 𝑋 ) )
19 18 elpwid ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ⊆ ( 𝑋 × 𝑋 ) )