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 24774
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 24771 . 2 class CMet
2 vx . . 3 setvar π‘₯
3 cvv 3475 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1541 . . . . . . . 8 class 𝑑
6 cmopn 20934 . . . . . . . 8 class MetOpen
75, 6cfv 6544 . . . . . . 7 class (MetOpenβ€˜π‘‘)
8 vf . . . . . . . 8 setvar 𝑓
98cv 1541 . . . . . . 7 class 𝑓
10 cflim 23438 . . . . . . 7 class fLim
117, 9, 10co 7409 . . . . . 6 class ((MetOpenβ€˜π‘‘) fLim 𝑓)
12 c0 4323 . . . . . 6 class βˆ…
1311, 12wne 2941 . . . . 5 wff ((MetOpenβ€˜π‘‘) fLim 𝑓) β‰  βˆ…
14 ccfil 24769 . . . . . 6 class CauFil
155, 14cfv 6544 . . . . 5 class (CauFilβ€˜π‘‘)
1613, 8, 15wral 3062 . . . 4 wff βˆ€π‘“ ∈ (CauFilβ€˜π‘‘)((MetOpenβ€˜π‘‘) fLim 𝑓) β‰  βˆ…
172cv 1541 . . . . 5 class π‘₯
18 cmet 20930 . . . . 5 class Met
1917, 18cfv 6544 . . . 4 class (Metβ€˜π‘₯)
2016, 4, 19crab 3433 . . 3 class {𝑑 ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘“ ∈ (CauFilβ€˜π‘‘)((MetOpenβ€˜π‘‘) fLim 𝑓) β‰  βˆ…}
212, 3, 20cmpt 5232 . 2 class (π‘₯ ∈ V ↦ {𝑑 ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘“ ∈ (CauFilβ€˜π‘‘)((MetOpenβ€˜π‘‘) fLim 𝑓) β‰  βˆ…})
221, 21wceq 1542 1 wff CMet = (π‘₯ ∈ V ↦ {𝑑 ∈ (Metβ€˜π‘₯) ∣ βˆ€π‘“ ∈ (CauFilβ€˜π‘‘)((MetOpenβ€˜π‘‘) fLim 𝑓) β‰  βˆ…})
Colors of variables: wff setvar class
This definition is referenced by:  iscmet  24801
  Copyright terms: Public domain W3C validator