Metamath Proof Explorer

Theorem cuspusp

Description: A complete uniform space is an 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⁡BaseWc∈CauFilU⁡UnifSt⁡W→TopOpen⁡WfLimc≠∅
2 1 simplbi ⊢W∈CUnifSp→W∈UnifSp