Metamath Proof Explorer

Theorem iscusp

Description: The predicate " W is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017)

Ref Expression
Assertion iscusp ⊢W∈CUnifSp↔W∈UnifSp∧∀c∈Fil⁡BaseWc∈CauFilU⁡UnifSt⁡W→TopOpen⁡WfLimc≠∅

Proof

Step Hyp Ref Expression
1 2fveq3 ⊢w=W→Fil⁡Basew=Fil⁡BaseW
2 2fveq3 ⊢w=W→CauFilU⁡UnifSt⁡w=CauFilU⁡UnifSt⁡W
3 2 eleq2d ⊢w=W→c∈CauFilU⁡UnifSt⁡w↔c∈CauFilU⁡UnifSt⁡W
4 fveq2 ⊢w=W→TopOpen⁡w=TopOpen⁡W
5 4 oveq1d ⊢w=W→TopOpen⁡wfLimc=TopOpen⁡WfLimc
6 5 neeq1d ⊢w=W→TopOpen⁡wfLimc≠∅↔TopOpen⁡WfLimc≠∅
7 3 6 imbi12d ⊢w=W→c∈CauFilU⁡UnifSt⁡w→TopOpen⁡wfLimc≠∅↔c∈CauFilU⁡UnifSt⁡W→TopOpen⁡WfLimc≠∅
8 1 7 raleqbidv ⊢w=W→∀c∈Fil⁡Basewc∈CauFilU⁡UnifSt⁡w→TopOpen⁡wfLimc≠∅↔∀c∈Fil⁡BaseWc∈CauFilU⁡UnifSt⁡W→TopOpen⁡WfLimc≠∅
9 df-cusp ⊢CUnifSp=w∈UnifSp|∀c∈Fil⁡Basewc∈CauFilU⁡UnifSt⁡w→TopOpen⁡wfLimc≠∅
10 8 9 elrab2 ⊢W∈CUnifSp↔W∈UnifSp∧∀c∈Fil⁡BaseWc∈CauFilU⁡UnifSt⁡W→TopOpen⁡WfLimc≠∅