Definition df-cmet 24402

Description: Define the set of complete metrics on a given set. (Contributed by Mario Carneiro, 1-May-2014.)

Assertion

Ref	Expression
df-cmet	⊢ CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})

Distinct variable group:   𝑓,𝑑,𝑥

Detailed syntax breakdown of Definition df-cmet

Step	Hyp	Ref	Expression
1		ccmet 24399	. 2 class CMet
2		vx	. . 3 setvar 𝑥
3		cvv 3430	. . 3 class V
4		vd	. . . . . . . . 9 setvar 𝑑
5	4	cv 1540	. . . . . . . 8 class 𝑑
6		cmopn 20568	. . . . . . . 8 class MetOpen
7	5, 6	cfv 6430	. . . . . . 7 class (MetOpen‘𝑑)
8		vf	. . . . . . . 8 setvar 𝑓
9	8	cv 1540	. . . . . . 7 class 𝑓
10		cflim 23066	. . . . . . 7 class fLim
11	7, 9, 10	co 7268	. . . . . 6 class ((MetOpen‘𝑑) fLim 𝑓)
12		c0 4261	. . . . . 6 class ∅
13	11, 12	wne 2944	. . . . 5 wff ((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
14		ccfil 24397	. . . . . 6 class CauFil
15	5, 14	cfv 6430	. . . . 5 class (CauFil‘𝑑)
16	13, 8, 15	wral 3065	. . . 4 wff ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
17	2	cv 1540	. . . . 5 class 𝑥
18		cmet 20564	. . . . 5 class Met
19	17, 18	cfv 6430	. . . 4 class (Met‘𝑥)
20	16, 4, 19	crab 3069	. . 3 class {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}
21	2, 3, 20	cmpt 5161	. 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
22	1, 21	wceq 1541	1 wff CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})

This definition is referenced by:  iscmet  24429