Definition df-cfil 19169

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 19166	. 2 class CauFil
2		vd	. . 3 set d
3		cxmt 16649	. . . . 5 class * Met
4	3	crn 4846	. . . 4 class ran * Met
5	4	cuni 3983	. . 3 class U. ran * Met
6	2	cv 1648	. . . . . . . 8 class d
7		vy	. . . . . . . . . 10 set y
8	7	cv 1648	. . . . . . . . 9 class y
9	8, 8	cxp 4843	. . . . . . . 8 class ( y X. y )
10	6, 9	cima 4848	. . . . . . 7 class ( d " ( y X. y ) )
11		cc0 8954	. . . . . . . 8 class 0
12		vx	. . . . . . . . 9 set x
13	12	cv 1648	. . . . . . . 8 class x
14		cico 10882	. . . . . . . 8 class [,)
15	11, 13, 14	co 6048	. . . . . . 7 class ( 0 [,) x )
16	10, 15	wss 3288	. . . . . 6 wff ( d " ( y X. y ) ) C_ ( 0 [,) x )
17		vf	. . . . . . 7 set f
18	17	cv 1648	. . . . . 6 class f
19	16, 7, 18	wrex 2675	. . . . 5 wff E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
20		crp 10576	. . . . 5 class RR+
21	19, 12, 20	wral 2674	. . . 4 wff A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
22	6	cdm 4845	. . . . . 6 class dom d
23	22	cdm 4845	. . . . 5 class dom dom d
24		cfil 17838	. . . . 5 class Fil
25	23, 24	cfv 5421	. . . 4 class ( Fil ` dom dom d )
26	21, 17, 25	crab 2678	. . 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 4234	. 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 1649	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  19178  cfili  19182  cfilfcls  19188