Metamath Proof Explorer

Theorem iscusp2

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

Ref Expression
Hypotheses iscusp2.1 
|- B = ( Base ` W )
iscusp2.2 
|- U = ( UnifSt ` W )
iscusp2.3 
|- J = ( TopOpen ` W )
Assertion iscusp2 
|- ( W e. CUnifSp <-> ( W e. UnifSp /\ A. c e. ( Fil ` B ) ( c e. ( CauFilU ` U ) -> ( J fLim c ) =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 iscusp2.1 
 |-  B = ( Base ` W )
2 iscusp2.2 
 |-  U = ( UnifSt ` W )
3 iscusp2.3 
 |-  J = ( TopOpen ` W )
4 iscusp 
 |-  ( W e. CUnifSp <-> ( W e. UnifSp /\ A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) ) )
5 1 fveq2i 
 |-  ( Fil ` B ) = ( Fil ` ( Base ` W ) )
6 2 fveq2i 
 |-  ( CauFilU ` U ) = ( CauFilU ` ( UnifSt ` W ) )
7 6 eleq2i 
 |-  ( c e. ( CauFilU ` U ) <-> c e. ( CauFilU ` ( UnifSt ` W ) ) )
8 3 oveq1i 
 |-  ( J fLim c ) = ( ( TopOpen ` W ) fLim c )
9 8 neeq1i 
 |-  ( ( J fLim c ) =/= (/) <-> ( ( TopOpen ` W ) fLim c ) =/= (/) )
10 7 9 imbi12i 
 |-  ( ( c e. ( CauFilU ` U ) -> ( J fLim c ) =/= (/) ) <-> ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) )
11 5 10 raleqbii 
 |-  ( A. c e. ( Fil ` B ) ( c e. ( CauFilU ` U ) -> ( J fLim c ) =/= (/) ) <-> A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) )
12 11 anbi2i 
 |-  ( ( W e. UnifSp /\ A. c e. ( Fil ` B ) ( c e. ( CauFilU ` U ) -> ( J fLim c ) =/= (/) ) ) <-> ( W e. UnifSp /\ A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) ) )
13 4 12 bitr4i 
 |-  ( W e. CUnifSp <-> ( W e. UnifSp /\ A. c e. ( Fil ` B ) ( c e. ( CauFilU ` U ) -> ( J fLim c ) =/= (/) ) ) )