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 = ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( Fil ‘ dom dom 𝑑 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccfil	⊢ CauFil
1		vd	⊢ 𝑑
2		cxmet	⊢ ∞Met
3	2	crn	⊢ ran ∞Met
4	3	cuni	⊢ ∪ ran ∞Met
5		vf	⊢ 𝑓
6		cfil	⊢ Fil
7	1	cv	⊢ 𝑑
8	7	cdm	⊢ dom 𝑑
9	8	cdm	⊢ dom dom 𝑑
10	9 6	cfv	⊢ ( Fil ‘ dom dom 𝑑 )
11		vx	⊢ 𝑥
12		crp	⊢ ℝ+
13		vy	⊢ 𝑦
14	5	cv	⊢ 𝑓
15	13	cv	⊢ 𝑦
16	15 15	cxp	⊢ ( 𝑦 × 𝑦 )
17	7 16	cima	⊢ ( 𝑑 “ ( 𝑦 × 𝑦 ) )
18		cc0	⊢ 0
19		cico	⊢ [,)
20	11	cv	⊢ 𝑥
21	18 20 19	co	⊢ ( 0 [,) 𝑥 )
22	17 21	wss	⊢ ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 )
23	22 13 14	wrex	⊢ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 )
24	23 11 12	wral	⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 )
25	24 5 10	crab	⊢ { 𝑓 ∈ ( Fil ‘ dom dom 𝑑 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) }
26	1 4 25	cmpt	⊢ ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( Fil ‘ dom dom 𝑑 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )
27	0 26	wceq	⊢ CauFil = ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( Fil ‘ dom dom 𝑑 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )