Description: Elements of the filter base generated by the metric D are relations. (Contributed by Thierry Arnoux, 28-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | metust.1 | ⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) | |
| Assertion | metustrel | ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → Rel 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | metust.1 | ⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) | |
| 2 | 1 | metustss | ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ⊆ ( 𝑋 × 𝑋 ) ) |
| 3 | xpss | ⊢ ( 𝑋 × 𝑋 ) ⊆ ( V × V ) | |
| 4 | 2 3 | sstrdi | ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ⊆ ( V × V ) ) |
| 5 | df-rel | ⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) ) | |
| 6 | 4 5 | sylibr | ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → Rel 𝐴 ) |