This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ≠ ∅