Metamath Proof Explorer

Theorem cuspcvg

Description: In a complete uniform space, any Cauchy filter C has a limit. (Contributed by Thierry Arnoux, 3-Dec-2017)

Ref Expression
Hypotheses cuspcvg.1 ⊢B=BaseW
cuspcvg.2 ⊢J=TopOpen⁡W
Assertion cuspcvg ⊢W∈CUnifSp∧C∈CauFilU⁡UnifSt⁡W∧C∈Fil⁡B→JfLimC≠∅

Proof

Step Hyp Ref Expression
1 cuspcvg.1 ⊢B=BaseW
2 cuspcvg.2 ⊢J=TopOpen⁡W
3 eleq1 ⊢c=C→c∈CauFilU⁡UnifSt⁡W↔C∈CauFilU⁡UnifSt⁡W
4 2 eqcomi ⊢TopOpen⁡W=J
5 4 a1i ⊢c=C→TopOpen⁡W=J
6 id ⊢c=C→c=C
7 5 6 oveq12d ⊢c=C→TopOpen⁡WfLimc=JfLimC
8 7 neeq1d ⊢c=C→TopOpen⁡WfLimc≠∅↔JfLimC≠∅
9 3 8 imbi12d ⊢c=C→c∈CauFilU⁡UnifSt⁡W→TopOpen⁡WfLimc≠∅↔C∈CauFilU⁡UnifSt⁡W→JfLimC≠∅
10 iscusp ⊢W∈CUnifSp↔W∈UnifSp∧∀c∈Fil⁡BaseWc∈CauFilU⁡UnifSt⁡W→TopOpen⁡WfLimc≠∅
11 10 simprbi ⊢W∈CUnifSp→∀c∈Fil⁡BaseWc∈CauFilU⁡UnifSt⁡W→TopOpen⁡WfLimc≠∅
12 11 adantr ⊢W∈CUnifSp∧C∈Fil⁡B→∀c∈Fil⁡BaseWc∈CauFilU⁡UnifSt⁡W→TopOpen⁡WfLimc≠∅
13 simpr ⊢W∈CUnifSp∧C∈Fil⁡B→C∈Fil⁡B
14 1 fveq2i ⊢Fil⁡B=Fil⁡BaseW
15 13 14 eleqtrdi ⊢W∈CUnifSp∧C∈Fil⁡B→C∈Fil⁡BaseW
16 9 12 15 rspcdva ⊢W∈CUnifSp∧C∈Fil⁡B→C∈CauFilU⁡UnifSt⁡W→JfLimC≠∅
17 16 3impia ⊢W∈CUnifSp∧C∈Fil⁡B∧C∈CauFilU⁡UnifSt⁡W→JfLimC≠∅
18 17 3com23 ⊢W∈CUnifSp∧C∈CauFilU⁡UnifSt⁡W∧C∈Fil⁡B→JfLimC≠∅