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

Metamath Proof Explorer

Theorem metustrel

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	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
	Assertion	metustrel	$⊢ (D \in PsMet (X) \land A \in F) \to Rel A$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2	1	metustss	$⊢ (D \in PsMet (X) \land A \in F) \to A \subseteq X \times X$
3		xpss	$⊢ X \times X \subseteq V \times V$
4	2 3	sstrdi	$⊢ (D \in PsMet (X) \land A \in F) \to A \subseteq V \times V$
5		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
6	4 5	sylibr	$⊢ (D \in PsMet (X) \land A \in F) \to Rel A$