cfilucfil2

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil . (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Assertion	cfilucfil2	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (C \in CauFilU (metUnif (D)) \leftrightarrow (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x)))$

Proof

Step	Hyp	Ref	Expression
1		metuval	$⊢ D \in PsMet (X) \to metUnif (D) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2	1	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to metUnif (D) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
3	2	fveq2d	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to CauFilU (metUnif (D)) = CauFilU ((X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]))$
4	3	eleq2d	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (C \in CauFilU (metUnif (D)) \leftrightarrow C \in CauFilU ((X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])))$
5		oveq2	$⊢ a = b \to [0, a) = [0, b)$
6	5	imaeq2d	$⊢ a = b \to D^{-1} [[0, a)] = D^{-1} [[0, b)]$
7	6	cbvmptv	$⊢ (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
8	7	rneqi	$⊢ ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
9	8	cfilucfil	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (C \in CauFilU ((X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \leftrightarrow (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x)))$
10	4 9	bitrd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (C \in CauFilU (metUnif (D)) \leftrightarrow (C \in fBas (X) \land \forall x \in ℝ^{+} \exists y \in C D [y \times y] \subseteq [0, x)))$

Metamath Proof Explorer

Theorem cfilucfil2

Proof