MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cmet Structured version   Visualization version   GIF version

Definition df-cmet 22808
Description: Define the class of complete metrics. (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
StepHypRef Expression
1 cms 22805 . 2 class CMet
2 vx . . 3 setvar 𝑥
3 cvv 3173 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1474 . . . . . . . 8 class 𝑑
6 cmopn 19506 . . . . . . . 8 class MetOpen
75, 6cfv 5790 . . . . . . 7 class (MetOpen‘𝑑)
8 vf . . . . . . . 8 setvar 𝑓
98cv 1474 . . . . . . 7 class 𝑓
10 cflim 21496 . . . . . . 7 class fLim
117, 9, 10co 6527 . . . . . 6 class ((MetOpen‘𝑑) fLim 𝑓)
12 c0 3874 . . . . . 6 class
1311, 12wne 2780 . . . . 5 wff ((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
14 ccfil 22803 . . . . . 6 class CauFil
155, 14cfv 5790 . . . . 5 class (CauFil‘𝑑)
1613, 8, 15wral 2896 . . . 4 wff 𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
172cv 1474 . . . . 5 class 𝑥
18 cme 19502 . . . . 5 class Met
1917, 18cfv 5790 . . . 4 class (Met‘𝑥)
2016, 4, 19crab 2900 . . 3 class {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}
212, 3, 20cmpt 4638 . 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
221, 21wceq 1475 1 wff CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
Colors of variables: wff setvar class
This definition is referenced by:  iscmet  22835
  Copyright terms: Public domain W3C validator