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

Theorem iscusp 23052
Description: The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017.)
Assertion
Ref Expression
iscusp (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘(Base‘𝑊))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)))
Distinct variable group:   𝑊,𝑐

Proof of Theorem iscusp
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 2fveq3 6680 . . 3 (𝑤 = 𝑊 → (Fil‘(Base‘𝑤)) = (Fil‘(Base‘𝑊)))
2 2fveq3 6680 . . . . 5 (𝑤 = 𝑊 → (CauFilu‘(UnifSt‘𝑤)) = (CauFilu‘(UnifSt‘𝑊)))
32eleq2d 2818 . . . 4 (𝑤 = 𝑊 → (𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) ↔ 𝑐 ∈ (CauFilu‘(UnifSt‘𝑊))))
4 fveq2 6675 . . . . . 6 (𝑤 = 𝑊 → (TopOpen‘𝑤) = (TopOpen‘𝑊))
54oveq1d 7186 . . . . 5 (𝑤 = 𝑊 → ((TopOpen‘𝑤) fLim 𝑐) = ((TopOpen‘𝑊) fLim 𝑐))
65neeq1d 2993 . . . 4 (𝑤 = 𝑊 → (((TopOpen‘𝑤) fLim 𝑐) ≠ ∅ ↔ ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅))
73, 6imbi12d 348 . . 3 (𝑤 = 𝑊 → ((𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅) ↔ (𝑐 ∈ (CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)))
81, 7raleqbidv 3304 . 2 (𝑤 = 𝑊 → (∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅) ↔ ∀𝑐 ∈ (Fil‘(Base‘𝑊))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)))
9 df-cusp 23051 . 2 CUnifSp = {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)}
108, 9elrab2 3591 1 (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘(Base‘𝑊))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wcel 2113  wne 2934  wral 3053  c0 4212  cfv 6340  (class class class)co 7171  Basecbs 16587  TopOpenctopn 16799  Filcfil 22597   fLim cflim 22686  UnifStcuss 23006  UnifSpcusp 23007  CauFiluccfilu 23039  CUnifSpccusp 23050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rab 3062  df-v 3400  df-un 3849  df-in 3851  df-ss 3861  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-iota 6298  df-fv 6348  df-ov 7174  df-cusp 23051
This theorem is referenced by:  cuspusp  23053  cuspcvg  23054  iscusp2  23055  cmetcusp  24107
  Copyright terms: Public domain W3C validator