Metamath Proof Explorer

Definition df-cmet

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

Ref Expression
Assertion df-cmet ⊢ CMet = x ∈ V ⟼ d ∈ Met ⁡ x | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmet class CMet
1 vx setvar x
2 cvv class V
3 vd setvar d
4 cmet class Met
5 1 cv setvar x
6 5 4 cfv class Met ⁡ x
7 vf setvar f
8 ccfil class CauFil
9 3 cv setvar d
10 9 8 cfv class CauFil ⁡ d
11 cmopn class MetOpen
12 9 11 cfv class MetOpen ⁡ d
13 cflim class fLim
14 7 cv setvar f
15 12 14 13 co class MetOpen ⁡ d fLim f
16 c0 class ∅
17 15 16 wne wff MetOpen ⁡ d fLim f ≠ ∅
18 17 7 10 wral wff ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅
19 18 3 6 crab class d ∈ Met ⁡ x | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅
20 1 2 19 cmpt class x ∈ V ⟼ d ∈ Met ⁡ x | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅
21 0 20 wceq wff CMet = x ∈ V ⟼ d ∈ Met ⁡ x | ∀ f ∈ CauFil ⁡ d MetOpen ⁡ d fLim f ≠ ∅