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 ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ⊆ ( 𝑋 × 𝑋 ) )