This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 [,) 𝑥 ) } )