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 Base W c CauFilU UnifSt W TopOpen W fLim c
2 1 simplbi W CUnifSp W UnifSp