Metamath Proof Explorer

Theorem iscusp

Description: The predicate " W is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017)

Ref Expression
Assertion iscusp 
|- ( W e. CUnifSp <-> ( W e. UnifSp /\ A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 2fveq3 
 |-  ( w = W -> ( Fil ` ( Base ` w ) ) = ( Fil ` ( Base ` W ) ) )
2 2fveq3 
 |-  ( w = W -> ( CauFilU ` ( UnifSt ` w ) ) = ( CauFilU ` ( UnifSt ` W ) ) )
3 2 eleq2d 
 |-  ( w = W -> ( c e. ( CauFilU ` ( UnifSt ` w ) ) <-> c e. ( CauFilU ` ( UnifSt ` W ) ) ) )
4 fveq2 
 |-  ( w = W -> ( TopOpen ` w ) = ( TopOpen ` W ) )
5 4 oveq1d 
 |-  ( w = W -> ( ( TopOpen ` w ) fLim c ) = ( ( TopOpen ` W ) fLim c ) )
6 5 neeq1d 
 |-  ( w = W -> ( ( ( TopOpen ` w ) fLim c ) =/= (/) <-> ( ( TopOpen ` W ) fLim c ) =/= (/) ) )
7 3 6 imbi12d 
 |-  ( w = W -> ( ( c e. ( CauFilU ` ( UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) <-> ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) ) )
8 1 7 raleqbidv 
 |-  ( w = W -> ( A. c e. ( Fil ` ( Base ` w ) ) ( c e. ( CauFilU ` ( UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) <-> A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) ) )
9 df-cusp 
 |-  CUnifSp = { w e. UnifSp | A. c e. ( Fil ` ( Base ` w ) ) ( c e. ( CauFilU ` ( UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) }
10 8 9 elrab2 
 |-  ( W e. CUnifSp <-> ( W e. UnifSp /\ A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) ) )