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 e. CUnifSp /\ C e. ( CauFilU ` ( UnifSt ` W ) ) /\ C e. ( 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 e. ( CauFilU ` ( UnifSt ` W ) ) <-> C e. ( 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 e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) <-> ( C e. ( CauFilU ` ( UnifSt ` W ) ) -> ( J fLim C ) =/= (/) ) ) )
10 iscusp 
 |-  ( W e. CUnifSp <-> ( W e. UnifSp /\ A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) ) )
11 10 simprbi 
 |-  ( W e. CUnifSp -> A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) )
12 11 adantr 
 |-  ( ( W e. CUnifSp /\ C e. ( Fil ` B ) ) -> A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) )
13 simpr 
 |-  ( ( W e. CUnifSp /\ C e. ( Fil ` B ) ) -> C e. ( Fil ` B ) )
14 1 fveq2i 
 |-  ( Fil ` B ) = ( Fil ` ( Base ` W ) )
15 13 14 eleqtrdi 
 |-  ( ( W e. CUnifSp /\ C e. ( Fil ` B ) ) -> C e. ( Fil ` ( Base ` W ) ) )
16 9 12 15 rspcdva 
 |-  ( ( W e. CUnifSp /\ C e. ( Fil ` B ) ) -> ( C e. ( CauFilU ` ( UnifSt ` W ) ) -> ( J fLim C ) =/= (/) ) )
17 16 3impia 
 |-  ( ( W e. CUnifSp /\ C e. ( Fil ` B ) /\ C e. ( CauFilU ` ( UnifSt ` W ) ) ) -> ( J fLim C ) =/= (/) )
18 17 3com23 
 |-  ( ( W e. CUnifSp /\ C e. ( CauFilU ` ( UnifSt ` W ) ) /\ C e. ( Fil ` B ) ) -> ( J fLim C ) =/= (/) )