Definition 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 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 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccfil	|- CauFil
1		vd	|- d
2		cxmet	|- *Met
3	2	crn	|- ran *Met
4	3	cuni	|- U. ran *Met
5		vf	|- f
6		cfil	|- Fil
7	1	cv	|- d
8	7	cdm	|- dom d
9	8	cdm	|- dom dom d
10	9 6	cfv	|- ( Fil ` dom dom d )
11		vx	|- x
12		crp	|- RR+
13		vy	|- y
14	5	cv	|- f
15	13	cv	|- y
16	15 15	cxp	|- ( y X. y )
17	7 16	cima	|- ( d " ( y X. y ) )
18		cc0	|- 0
19		cico	|- [,)
20	11	cv	|- x
21	18 20 19	co	|- ( 0 [,) x )
22	17 21	wss	|- ( d " ( y X. y ) ) C_ ( 0 [,) x )
23	22 13 14	wrex	|- E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
24	23 11 12	wral	|- A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
25	24 5 10	crab	|- { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) }
26	1 4 25	cmpt	|- ( 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 ) } )
27	0 26	wceq	|- 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 ) } )