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

Definition df-cmet 23101
 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 23098 . 2 class CMet
2 vx . . 3 setvar 𝑥
3 cvv 3231 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1522 . . . . . . . 8 class 𝑑
6 cmopn 19784 . . . . . . . 8 class MetOpen
75, 6cfv 5926 . . . . . . 7 class (MetOpen‘𝑑)
8 vf . . . . . . . 8 setvar 𝑓
98cv 1522 . . . . . . 7 class 𝑓
10 cflim 21785 . . . . . . 7 class fLim
117, 9, 10co 6690 . . . . . 6 class ((MetOpen‘𝑑) fLim 𝑓)
12 c0 3948 . . . . . 6 class
1311, 12wne 2823 . . . . 5 wff ((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
14 ccfil 23096 . . . . . 6 class CauFil
155, 14cfv 5926 . . . . 5 class (CauFil‘𝑑)
1613, 8, 15wral 2941 . . . 4 wff 𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
172cv 1522 . . . . 5 class 𝑥
18 cme 19780 . . . . 5 class Met
1917, 18cfv 5926 . . . 4 class (Met‘𝑥)
2016, 4, 19crab 2945 . . 3 class {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}
212, 3, 20cmpt 4762 . 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
221, 21wceq 1523 1 wff CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
 Colors of variables: wff setvar class This definition is referenced by:  iscmet  23128
 Copyright terms: Public domain W3C validator