Theorem cuspusp

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

	Ref	Expression
Assertion	cuspusp	⊢ ( 𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp )

Proof

Step	Hyp	Ref	Expression
1		iscusp	⊢ ( 𝑊 ∈ CUnifSp ↔ ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )
2	1	simplbi	⊢ ( 𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp )