Metamath Proof Explorer

Theorem cfilfval

Description: The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015)

		Ref	Expression
	Assertion	cfilfval	$⊢ D \in ∞Met (X) \to CauFil (D) = \{f \in Fil (X) \| \forall x \in ℝ^{+} \exists y \in f D [y \times y] \subseteq [0, x)\}$

Proof

Step	Hyp	Ref	Expression
1		fvssunirn	$⊢ ∞Met (X) \subseteq ⋃ ran ∞Met$
2	1	sseli	$⊢ D \in ∞Met (X) \to D \in ⋃ ran ∞Met$
3		dmeq	$⊢ d = D \to dom d = dom D$
4	3	dmeqd	$⊢ d = D \to dom dom d = dom dom D$
5	4	fveq2d	$⊢ d = D \to Fil (dom dom d) = Fil (dom dom D)$
6		imaeq1	$⊢ d = D \to d [y \times y] = D [y \times y]$
7	6	sseq1d	$⊢ d = D \to (d [y \times y] \subseteq [0, x) \leftrightarrow D [y \times y] \subseteq [0, x))$
8	7	rexbidv	$⊢ d = D \to (\exists y \in f d [y \times y] \subseteq [0, x) \leftrightarrow \exists y \in f D [y \times y] \subseteq [0, x))$
9	8	ralbidv	$⊢ d = D \to (\forall x \in ℝ^{+} \exists y \in f d [y \times y] \subseteq [0, x) \leftrightarrow \forall x \in ℝ^{+} \exists y \in f D [y \times y] \subseteq [0, x))$
10	5 9	rabeqbidv	$⊢ d = D \to \{f \in Fil (dom dom d) \| \forall x \in ℝ^{+} \exists y \in f d [y \times y] \subseteq [0, x)\} = \{f \in Fil (dom dom D) \| \forall x \in ℝ^{+} \exists y \in f D [y \times y] \subseteq [0, x)\}$
11		df-cfil	$⊢ CauFil = (d \in ⋃ ran ∞Met ⟼ \{f \in Fil (dom dom d) \| \forall x \in ℝ^{+} \exists y \in f d [y \times y] \subseteq [0, x)\})$
12		fvex	$⊢ Fil (dom dom D) \in V$
13	12	rabex	$⊢ \{f \in Fil (dom dom D) \| \forall x \in ℝ^{+} \exists y \in f D [y \times y] \subseteq [0, x)\} \in V$
14	10 11 13	fvmpt	$⊢ D \in ⋃ ran ∞Met \to CauFil (D) = \{f \in Fil (dom dom D) \| \forall x \in ℝ^{+} \exists y \in f D [y \times y] \subseteq [0, x)\}$
15	2 14	syl	$⊢ D \in ∞Met (X) \to CauFil (D) = \{f \in Fil (dom dom D) \| \forall x \in ℝ^{+} \exists y \in f D [y \times y] \subseteq [0, x)\}$
16		xmetdmdm	$⊢ D \in ∞Met (X) \to X = dom dom D$
17	16	fveq2d	$⊢ D \in ∞Met (X) \to Fil (X) = Fil (dom dom D)$
18	17	rabeqdv	$⊢ D \in ∞Met (X) \to \{f \in Fil (X) \| \forall x \in ℝ^{+} \exists y \in f D [y \times y] \subseteq [0, x)\} = \{f \in Fil (dom dom D) \| \forall x \in ℝ^{+} \exists y \in f D [y \times y] \subseteq [0, x)\}$
19	15 18	eqtr4d	$⊢ D \in ∞Met (X) \to CauFil (D) = \{f \in Fil (X) \| \forall x \in ℝ^{+} \exists y \in f D [y \times y] \subseteq [0, x)\}$