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

Definition df-cmet 23871
 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
StepHypRef Expression
1 ccmet 23868 . 2 class CMet
2 vx . . 3 setvar 𝑥
3 cvv 3441 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1537 . . . . . . . 8 class 𝑑
6 cmopn 20085 . . . . . . . 8 class MetOpen
75, 6cfv 6325 . . . . . . 7 class (MetOpen‘𝑑)
8 vf . . . . . . . 8 setvar 𝑓
98cv 1537 . . . . . . 7 class 𝑓
10 cflim 22549 . . . . . . 7 class fLim
117, 9, 10co 7136 . . . . . 6 class ((MetOpen‘𝑑) fLim 𝑓)
12 c0 4243 . . . . . 6 class
1311, 12wne 2987 . . . . 5 wff ((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
14 ccfil 23866 . . . . . 6 class CauFil
155, 14cfv 6325 . . . . 5 class (CauFil‘𝑑)
1613, 8, 15wral 3106 . . . 4 wff 𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅
172cv 1537 . . . . 5 class 𝑥
18 cmet 20081 . . . . 5 class Met
1917, 18cfv 6325 . . . 4 class (Met‘𝑥)
2016, 4, 19crab 3110 . . 3 class {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}
212, 3, 20cmpt 5111 . 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
221, 21wceq 1538 1 wff CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
 Colors of variables: wff setvar class This definition is referenced by:  iscmet  23898
 Copyright terms: Public domain W3C validator