Definition df-cfil 23858

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 23855	. 2 class CauFil
2		vd	. . 3 setvar 𝑑
3		cxmet 20530	. . . . 5 class ∞Met
4	3	crn 5556	. . . 4 class ran ∞Met
5	4	cuni 4838	. . 3 class ∪ ran ∞Met
6	2	cv 1536	. . . . . . . 8 class 𝑑
7		vy	. . . . . . . . . 10 setvar 𝑦
8	7	cv 1536	. . . . . . . . 9 class 𝑦
9	8, 8	cxp 5553	. . . . . . . 8 class (𝑦 × 𝑦)
10	6, 9	cima 5558	. . . . . . 7 class (𝑑 “ (𝑦 × 𝑦))
11		cc0 10537	. . . . . . . 8 class 0
12		vx	. . . . . . . . 9 setvar 𝑥
13	12	cv 1536	. . . . . . . 8 class 𝑥
14		cico 12741	. . . . . . . 8 class [,)
15	11, 13, 14	co 7156	. . . . . . 7 class (0[,)𝑥)
16	10, 15	wss 3936	. . . . . 6 wff (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
17		vf	. . . . . . 7 setvar 𝑓
18	17	cv 1536	. . . . . 6 class 𝑓
19	16, 7, 18	wrex 3139	. . . . 5 wff ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
20		crp 12390	. . . . 5 class ℝ+
21	19, 12, 20	wral 3138	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
22	6	cdm 5555	. . . . . 6 class dom 𝑑
23	22	cdm 5555	. . . . 5 class dom dom 𝑑
24		cfil 22453	. . . . 5 class Fil
25	23, 24	cfv 6355	. . . 4 class (Fil‘dom dom 𝑑)
26	21, 17, 25	crab 3142	. . 3 class {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}
27	2, 5, 26	cmpt 5146	. 2 class (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
28	1, 27	wceq 1537	1 wff CauFil = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})

This definition is referenced by:  cfilfval  23867  cfili  23871  cfilfcls  23877