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 23267
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 23264 . 2 class CMet
2 vx . . 3 setvar 𝑥
3 cvv 3391 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1636 . . . . . . . 8 class 𝑑
6 cmopn 19944 . . . . . . . 8 class MetOpen
75, 6cfv 6101 . . . . . . 7 class (MetOpen‘𝑑)
8 vf . . . . . . . 8 setvar 𝑓
98cv 1636 . . . . . . 7 class 𝑓
10 cflim 21951 . . . . . . 7 class fLim
117, 9, 10co 6874 . . . . . 6 class ((MetOpen‘𝑑) fLim 𝑓)
12 c0 4116 . . . . . 6 class
1311, 12wne 2978 . . . . 5 wff ((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
14 ccfil 23262 . . . . . 6 class CauFil
155, 14cfv 6101 . . . . 5 class (CauFil‘𝑑)
1613, 8, 15wral 3096 . . . 4 wff 𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
172cv 1636 . . . . 5 class 𝑥
18 cme 19940 . . . . 5 class Met
1917, 18cfv 6101 . . . 4 class (Met‘𝑥)
2016, 4, 19crab 3100 . . 3 class {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}
212, 3, 20cmpt 4923 . 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
221, 21wceq 1637 1 wff CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
Colors of variables: wff setvar class
This definition is referenced by:  iscmet  23294
  Copyright terms: Public domain W3C validator