Definition df-cfil 23053

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 23050	. 2 class CauFil
2		vd	. . 3 setvar d
3		cxmt 19731	. . . . 5 class *Met
4	3	crn 5115	. . . 4 class ran *Met
5	4	cuni 4436	. . 3 class U. ran *Met
6	2	cv 1482	. . . . . . . 8 class d
7		vy	. . . . . . . . . 10 setvar y
8	7	cv 1482	. . . . . . . . 9 class y
9	8, 8	cxp 5112	. . . . . . . 8 class ( y X. y )
10	6, 9	cima 5117	. . . . . . 7 class ( d " ( y X. y ) )
11		cc0 9936	. . . . . . . 8 class 0
12		vx	. . . . . . . . 9 setvar x
13	12	cv 1482	. . . . . . . 8 class x
14		cico 12177	. . . . . . . 8 class [,)
15	11, 13, 14	co 6650	. . . . . . 7 class ( 0 [,) x )
16	10, 15	wss 3574	. . . . . 6 wff ( d " ( y X. y ) ) C_ ( 0 [,) x )
17		vf	. . . . . . 7 setvar f
18	17	cv 1482	. . . . . 6 class f
19	16, 7, 18	wrex 2913	. . . . 5 wff E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
20		crp 11832	. . . . 5 class RR+
21	19, 12, 20	wral 2912	. . . 4 wff A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
22	6	cdm 5114	. . . . . 6 class dom d
23	22	cdm 5114	. . . . 5 class dom dom d
24		cfil 21649	. . . . 5 class Fil
25	23, 24	cfv 5888	. . . 4 class ( Fil ` dom dom d )
26	21, 17, 25	crab 2916	. . 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 4729	. 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 1483	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  23062  cfili  23066  cfilfcls  23072