Definition df-cfil 25205

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 25202	. 2 class CauFil
2		vd	. . 3 setvar 𝑑
3		cxmet 21298	. . . . 5 class ∞Met
4	3	crn 5655	. . . 4 class ran ∞Met
5	4	cuni 4883	. . 3 class ∪ ran ∞Met
6	2	cv 1539	. . . . . . . 8 class 𝑑
7		vy	. . . . . . . . . 10 setvar 𝑦
8	7	cv 1539	. . . . . . . . 9 class 𝑦
9	8, 8	cxp 5652	. . . . . . . 8 class (𝑦 × 𝑦)
10	6, 9	cima 5657	. . . . . . 7 class (𝑑 “ (𝑦 × 𝑦))
11		cc0 11127	. . . . . . . 8 class 0
12		vx	. . . . . . . . 9 setvar 𝑥
13	12	cv 1539	. . . . . . . 8 class 𝑥
14		cico 13362	. . . . . . . 8 class [,)
15	11, 13, 14	co 7403	. . . . . . 7 class (0[,)𝑥)
16	10, 15	wss 3926	. . . . . 6 wff (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
17		vf	. . . . . . 7 setvar 𝑓
18	17	cv 1539	. . . . . 6 class 𝑓
19	16, 7, 18	wrex 3060	. . . . 5 wff ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
20		crp 13006	. . . . 5 class ℝ+
21	19, 12, 20	wral 3051	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
22	6	cdm 5654	. . . . . 6 class dom 𝑑
23	22	cdm 5654	. . . . 5 class dom dom 𝑑
24		cfil 23781	. . . . 5 class Fil
25	23, 24	cfv 6530	. . . 4 class (Fil‘dom dom 𝑑)
26	21, 17, 25	crab 3415	. . 3 class {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}
27	2, 5, 26	cmpt 5201	. 2 class (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
28	1, 27	wceq 1540	1 wff CauFil = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})

This definition is referenced by:  cfilfval  25214  cfili  25218  cfilfcls  25224