Metamath Proof Explorer

Theorem cuspusp

Description: A complete uniform space is a uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017)

Ref Expression
Assertion cuspusp ⊢ W ∈ CUnifSp → W ∈ UnifSp

Proof

Step Hyp Ref Expression
1 iscusp ⊢ W ∈ CUnifSp ↔ W ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ Base W c ∈ CauFilU ⁡ UnifSt ⁡ W → TopOpen ⁡ W fLim c ≠ ∅
2 1 simplbi ⊢ W ∈ CUnifSp → W ∈ UnifSp