Metamath Proof Explorer

Theorem metustel

Description: Define a filter base F generated by a metric D . (Contributed by Thierry Arnoux, 22-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
	Assertion	metustel	$⊢ D \in PsMet (X) \to (B \in F \leftrightarrow \exists a \in ℝ^{+} B = D^{-1} [[0, a)])$

Proof

Step	Hyp	Ref	Expression
1		metust.1	$⊢ F = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2	1	eleq2i	$⊢ B \in F \leftrightarrow B \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
3		elex	$⊢ B \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \to B \in V$
4	3	a1i	$⊢ D \in PsMet (X) \to (B \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \to B \in V)$
5		cnvexg	$⊢ D \in PsMet (X) \to D^{-1} \in V$
6		imaexg	$⊢ D^{-1} \in V \to D^{-1} [[0, a)] \in V$
7		eleq1a	$⊢ D^{-1} [[0, a)] \in V \to (B = D^{-1} [[0, a)] \to B \in V)$
8	5 6 7	3syl	$⊢ D \in PsMet (X) \to (B = D^{-1} [[0, a)] \to B \in V)$
9	8	rexlimdvw	$⊢ D \in PsMet (X) \to (\exists a \in ℝ^{+} B = D^{-1} [[0, a)] \to B \in V)$
10		eqid	$⊢ (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
11	10	elrnmpt	$⊢ B \in V \to (B \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} B = D^{-1} [[0, a)])$
12	11	a1i	$⊢ D \in PsMet (X) \to (B \in V \to (B \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} B = D^{-1} [[0, a)]))$
13	4 9 12	pm5.21ndd	$⊢ D \in PsMet (X) \to (B \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \leftrightarrow \exists a \in ℝ^{+} B = D^{-1} [[0, a)])$
14	2 13	bitrid	$⊢ D \in PsMet (X) \to (B \in F \leftrightarrow \exists a \in ℝ^{+} B = D^{-1} [[0, a)])$