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 ∧ 𝐶 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		cuspcvg.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		cuspcvg.2	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		eleq1	⊢ ( 𝑐 = 𝐶 → ( 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) ↔ 𝐶 ∈ ( CauFil_u ‘ ( 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	⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ↔ ( 𝐶 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ ) ) )
10		iscusp	⊢ ( 𝑊 ∈ CUnifSp ↔ ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )
11	10	simprbi	⊢ ( 𝑊 ∈ CUnifSp → ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) )
12	11	adantr	⊢ ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ) → ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFil_u ‘ ( 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 ‘ 𝐵 ) ) → ( 𝐶 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ ) )
17	16	3impia	⊢ ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ )
18	17	3com23	⊢ ( ( 𝑊 ∈ CUnifSp ∧ 𝐶 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) ∧ 𝐶 ∈ ( Fil ‘ 𝐵 ) ) → ( 𝐽 fLim 𝐶 ) ≠ ∅ )