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 [,) 𝑎 ) ) ) 𝑤𝑉 ) ) )