df-cfil

Description: Define the set of Cauchy filters on a given extended metric space. A Cauchy filter is a filter on the set such that for every 0 < x there is an element of the filter whose metric diameter is less than x . (Contributed by Mario Carneiro, 13-Oct-2015)

		Ref	Expression
	Assertion	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)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccfil	$class CauFil$
1		vd	$setvar d$
2		cxmet	$class ∞Met$
3	2	crn	$class ran ∞Met$
4	3	cuni	$class ⋃ ran ∞Met$
5		vf	$setvar f$
6		cfil	$class Fil$
7	1	cv	$setvar d$
8	7	cdm	$class dom d$
9	8	cdm	$class dom dom d$
10	9 6	cfv	$class Fil (dom dom d)$
11		vx	$setvar x$
12		crp	$class ℝ^{+}$
13		vy	$setvar y$
14	5	cv	$setvar f$
15	13	cv	$setvar y$
16	15 15	cxp	$class (y \times y)$
17	7 16	cima	$class d [y \times y]$
18		cc0	$class 0$
19		cico	$class [.)$
20	11	cv	$setvar x$
21	18 20 19	co	$class [0, x)$
22	17 21	wss	$wff d [y \times y] \subseteq [0, x)$
23	22 13 14	wrex	$wff \exists y \in f d [y \times y] \subseteq [0, x)$
24	23 11 12	wral	$wff \forall x \in ℝ^{+} \exists y \in f d [y \times y] \subseteq [0, x)$
25	24 5 10	crab	$class \{f \in Fil (dom dom d) \| \forall x \in ℝ^{+} \exists y \in f d [y \times y] \subseteq [0, x)\}$
26	1 4 25	cmpt	$class (d \in ⋃ ran ∞Met ⟼ \{f \in Fil (dom dom d) \| \forall x \in ℝ^{+} \exists y \in f d [y \times y] \subseteq [0, x)\})$
27	0 26	wceq	$wff 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)\})$

Metamath Proof Explorer

Definition df-cfil

Detailed syntax breakdown