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 = Base W
cuspcvg.2 J = TopOpen W
Assertion cuspcvg W CUnifSp C CauFilU UnifSt W C Fil B J fLim C

Proof

Step Hyp Ref Expression
1 cuspcvg.1 B = Base W
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 W fLim c = J fLim C
8 7 neeq1d c = C TopOpen W fLim c J fLim C
9 3 8 imbi12d c = C c CauFilU UnifSt W TopOpen W fLim c C CauFilU UnifSt W J fLim C
10 iscusp W CUnifSp W UnifSp c Fil Base W c CauFilU UnifSt W TopOpen W fLim c
11 10 simprbi W CUnifSp c Fil Base W c CauFilU UnifSt W TopOpen W fLim c
12 11 adantr W CUnifSp C Fil B c Fil Base W c CauFilU UnifSt W TopOpen W fLim c
13 simpr W CUnifSp C Fil B C Fil B
14 1 fveq2i Fil B = Fil Base W
15 13 14 eleqtrdi W CUnifSp C Fil B C Fil Base W
16 9 12 15 rspcdva W CUnifSp C Fil B C CauFilU UnifSt W J fLim C
17 16 3impia W CUnifSp C Fil B C CauFilU UnifSt W J fLim C
18 17 3com23 W CUnifSp C CauFilU UnifSt W C Fil B J fLim C