Definition df-cfil 24764

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 24761	. 2 class CauFil
2		vd	. . 3 setvar 𝑑
3		cxmet 20922	. . . . 5 class ∞Met
4	3	crn 5677	. . . 4 class ran ∞Met
5	4	cuni 4908	. . 3 class ∪ ran ∞Met
6	2	cv 1541	. . . . . . . 8 class 𝑑
7		vy	. . . . . . . . . 10 setvar 𝑦
8	7	cv 1541	. . . . . . . . 9 class 𝑦
9	8, 8	cxp 5674	. . . . . . . 8 class (𝑦 × 𝑦)
10	6, 9	cima 5679	. . . . . . 7 class (𝑑 “ (𝑦 × 𝑦))
11		cc0 11107	. . . . . . . 8 class 0
12		vx	. . . . . . . . 9 setvar 𝑥
13	12	cv 1541	. . . . . . . 8 class 𝑥
14		cico 13323	. . . . . . . 8 class [,)
15	11, 13, 14	co 7406	. . . . . . 7 class (0[,)𝑥)
16	10, 15	wss 3948	. . . . . 6 wff (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
17		vf	. . . . . . 7 setvar 𝑓
18	17	cv 1541	. . . . . 6 class 𝑓
19	16, 7, 18	wrex 3071	. . . . 5 wff ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
20		crp 12971	. . . . 5 class ℝ+
21	19, 12, 20	wral 3062	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)
22	6	cdm 5676	. . . . . 6 class dom 𝑑
23	22	cdm 5676	. . . . 5 class dom dom 𝑑
24		cfil 23341	. . . . 5 class Fil
25	23, 24	cfv 6541	. . . 4 class (Fil‘dom dom 𝑑)
26	21, 17, 25	crab 3433	. . 3 class {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}
27	2, 5, 26	cmpt 5231	. 2 class (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
28	1, 27	wceq 1542	1 wff CauFil = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})

This definition is referenced by:  cfilfval  24773  cfili  24777  cfilfcls  24783