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

Metamath Proof Explorer

Theorem metuel

Description: Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 8-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion metuel ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ ( metUnif ‘ 𝐷 ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 metuval ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )
2 1 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )
3 2 eleq2d ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ ( metUnif ‘ 𝐷 ) ↔ 𝑉 ∈ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ) )
4 oveq2 ⊢ ( 𝑎 = 𝑒 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑒 ) )
5 4 imaeq2d ⊢ ( 𝑎 = 𝑒 → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑒 ) ) )
6 5 cbvmptv ⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑒 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑒 ) ) )
7 6 rneqi ⊢ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑒 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑒 ) ) )
8 7 metustfbas ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
9 elfg ⊢ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ( 𝑉 ∈ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ) )
10 8 9 syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ) )
11 3 10 bitrd ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ ( metUnif ‘ 𝐷 ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ) )