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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
cuspcvg.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
Assertion cuspcvg ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 cuspcvg.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 cuspcvg.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3 eleq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) ↔ 𝐶 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) ) )
4 2 eqcomi ⊢ ( TopOpen ‘ 𝑊 ) = 𝐽
5 4 a1i ⊢ ( 𝑐 = 𝐶 → ( TopOpen ‘ 𝑊 ) = 𝐽 )
6 id ⊢ ( 𝑐 = 𝐶 → 𝑐 = 𝐶 )
7 5 6 oveq12d ⊢ ( 𝑐 = 𝐶 → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) = ( 𝐽 fLim 𝐶 ) )
8 7 neeq1d ⊢ ( 𝑐 = 𝐶 → ( ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ↔ ( 𝐽 fLim 𝐶 ) ≠ ∅ ) )
9 3 8 imbi12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ↔ ( 𝐶 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ ) ) )
10 iscusp ⊢ ( 𝑊 ∈ CUnifSp ↔ ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )
11 10 simprbi ⊢ ( 𝑊 ∈ CUnifSp → ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) )
12 11 adantr ⊢ ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ) → ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) )
13 simpr ⊢ ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ) → 𝐶 ∈ ( Fil ‘ 𝐵 ) )
14 1 fveq2i ⊢ ( Fil ‘ 𝐵 ) = ( Fil ‘ ( Base ‘ 𝑊 ) )
15 13 14 eleqtrdi ⊢ ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ) → 𝐶 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) )
16 9 12 15 rspcdva ⊢ ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ) → ( 𝐶 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ ) )
17 16 3impia ⊢ ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ∧ 𝐶 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ )
18 17 3com23 ⊢ ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ )