Definition df-cfil 24324

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 < 𝑥 there is an element of the filter whose metric diameter is less than 𝑥. (Contributed by Mario Carneiro, 13-Oct-2015.)

Assertion

Ref	Expression
df-cfil	⊢ CauFil = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})

Distinct variable group:   𝑓,𝑑,𝑥,𝑦

Detailed syntax breakdown of Definition df-cfil

Step	Hyp	Ref	Expression
1		ccfil 24321	. 2 class CauFil
2		vd	. . 3 setvar 𝑑
3		cxmet 20495	. . . . 5 class ∞Met
4	3	crn 5581	. . . 4 class ran ∞Met
5	4	cuni 4836	. . 3 class ∪ ran ∞Met
6	2	cv 1538	. . . . . . . 8 class 𝑑
7		vy	. . . . . . . . . 10 setvar 𝑦
8	7	cv 1538	. . . . . . . . 9 class 𝑦
9	8, 8	cxp 5578	. . . . . . . 8 class (𝑦 × 𝑦)
10	6, 9	cima 5583	. . . . . . 7 class (𝑑 “ (𝑦 × 𝑦))
11		cc0 10802	. . . . . . . 8 class 0
12		vx	. . . . . . . . 9 setvar 𝑥
13	12	cv 1538	. . . . . . . 8 class 𝑥
14		cico 13010	. . . . . . . 8 class [,)
15	11, 13, 14	co 7255	. . . . . . 7 class (0[,)𝑥)
16	10, 15	wss 3883	. . . . . 6 wff (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
17		vf	. . . . . . 7 setvar 𝑓
18	17	cv 1538	. . . . . 6 class 𝑓
19	16, 7, 18	wrex 3064	. . . . 5 wff ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
20		crp 12659	. . . . 5 class ℝ+
21	19, 12, 20	wral 3063	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
22	6	cdm 5580	. . . . . 6 class dom 𝑑
23	22	cdm 5580	. . . . 5 class dom dom 𝑑
24		cfil 22904	. . . . 5 class Fil
25	23, 24	cfv 6418	. . . 4 class (Fil‘dom dom 𝑑)
26	21, 17, 25	crab 3067	. . 3 class {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}
27	2, 5, 26	cmpt 5153	. 2 class (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
28	1, 27	wceq 1539	1 wff CauFil = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})

This definition is referenced by:  cfilfval  24333  cfili  24337  cfilfcls  24343