Definition df-cfil 19213

Description: Define the set of Cauchy filters on a 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.)

Assertion

Ref	Expression
df-cfil	|- CauFil = ( d e. U. ran * Met |-> { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) } )

Distinct variable group:   f, d, x, y

Detailed syntax breakdown of Definition df-cfil

Step	Hyp	Ref	Expression
1		ccfil 19210	. 2 class CauFil
2		vd	. . 3 set d
3		cxmt 16691	. . . . 5 class * Met
4	3	crn 4882	. . . 4 class ran * Met
5	4	cuni 4017	. . 3 class U. ran * Met
6	2	cv 1652	. . . . . . . 8 class d
7		vy	. . . . . . . . . 10 set y
8	7	cv 1652	. . . . . . . . 9 class y
9	8, 8	cxp 4879	. . . . . . . 8 class ( y X. y )
10	6, 9	cima 4884	. . . . . . 7 class ( d " ( y X. y ) )
11		cc0 8995	. . . . . . . 8 class 0
12		vx	. . . . . . . . 9 set x
13	12	cv 1652	. . . . . . . 8 class x
14		cico 10923	. . . . . . . 8 class [,)
15	11, 13, 14	co 6084	. . . . . . 7 class ( 0 [,) x )
16	10, 15	wss 3322	. . . . . 6 wff ( d " ( y X. y ) ) C_ ( 0 [,) x )
17		vf	. . . . . . 7 set f
18	17	cv 1652	. . . . . 6 class f
19	16, 7, 18	wrex 2708	. . . . 5 wff E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
20		crp 10617	. . . . 5 class RR+
21	19, 12, 20	wral 2707	. . . 4 wff A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
22	6	cdm 4881	. . . . . 6 class dom d
23	22	cdm 4881	. . . . 5 class dom dom d
24		cfil 17882	. . . . 5 class Fil
25	23, 24	cfv 5457	. . . 4 class ( Fil ` dom dom d )
26	21, 17, 25	crab 2711	. . 3 class { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) }
27	2, 5, 26	cmpt 4269	. 2 class ( d e. U. ran * Met |-> { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) } )
28	1, 27	wceq 1653	1 wff CauFil = ( d e. U. ran * Met |-> { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) } )

This definition is referenced by:  cfilfval  19222  cfili  19226  cfilfcls  19232