| 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 ) =/= (/) ) |