Definition df-cfil 23857

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 23854	. 2 class CauFil
2		vd	. . 3 setvar 𝑑
3		cxmet 20529	. . . . 5 class ∞Met
4	3	crn 5555	. . . 4 class ran ∞Met
5	4	cuni 4837	. . 3 class ∪ ran ∞Met
6	2	cv 1532	. . . . . . . 8 class 𝑑
7		vy	. . . . . . . . . 10 setvar 𝑦
8	7	cv 1532	. . . . . . . . 9 class 𝑦
9	8, 8	cxp 5552	. . . . . . . 8 class (𝑦 × 𝑦)
10	6, 9	cima 5557	. . . . . . 7 class (𝑑 “ (𝑦 × 𝑦))
11		cc0 10536	. . . . . . . 8 class 0
12		vx	. . . . . . . . 9 setvar 𝑥
13	12	cv 1532	. . . . . . . 8 class 𝑥
14		cico 12739	. . . . . . . 8 class [,)
15	11, 13, 14	co 7155	. . . . . . 7 class (0[,)𝑥)
16	10, 15	wss 3935	. . . . . 6 wff (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
17		vf	. . . . . . 7 setvar 𝑓
18	17	cv 1532	. . . . . 6 class 𝑓
19	16, 7, 18	wrex 3139	. . . . 5 wff ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
20		crp 12388	. . . . 5 class ℝ+
21	19, 12, 20	wral 3138	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
22	6	cdm 5554	. . . . . 6 class dom 𝑑
23	22	cdm 5554	. . . . 5 class dom dom 𝑑
24		cfil 22452	. . . . 5 class Fil
25	23, 24	cfv 6354	. . . 4 class (Fil‘dom dom 𝑑)
26	21, 17, 25	crab 3142	. . 3 class {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}
27	2, 5, 26	cmpt 5145	. 2 class (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
28	1, 27	wceq 1533	1 wff CauFil = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})

This definition is referenced by:  cfilfval  23866  cfili  23870  cfilfcls  23876