Metamath Proof Explorer


Theorem flimcls

Description: Closure in terms of filter convergence. (Contributed by Jeff Hankins, 28-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion flimcls JTopOnXSXAclsJSfFilXSfAJfLimf

Proof

Step Hyp Ref Expression
1 eqid XfilGenfineiJAS=XfilGenfineiJAS
2 1 flimclslem JTopOnXSXAclsJSXfilGenfineiJASFilXSXfilGenfineiJASAJfLimXfilGenfineiJAS
3 3anass XfilGenfineiJASFilXSXfilGenfineiJASAJfLimXfilGenfineiJASXfilGenfineiJASFilXSXfilGenfineiJASAJfLimXfilGenfineiJAS
4 2 3 sylib JTopOnXSXAclsJSXfilGenfineiJASFilXSXfilGenfineiJASAJfLimXfilGenfineiJAS
5 eleq2 f=XfilGenfineiJASSfSXfilGenfineiJAS
6 oveq2 f=XfilGenfineiJASJfLimf=JfLimXfilGenfineiJAS
7 6 eleq2d f=XfilGenfineiJASAJfLimfAJfLimXfilGenfineiJAS
8 5 7 anbi12d f=XfilGenfineiJASSfAJfLimfSXfilGenfineiJASAJfLimXfilGenfineiJAS
9 8 rspcev XfilGenfineiJASFilXSXfilGenfineiJASAJfLimXfilGenfineiJASfFilXSfAJfLimf
10 4 9 syl JTopOnXSXAclsJSfFilXSfAJfLimf
11 10 3expia JTopOnXSXAclsJSfFilXSfAJfLimf
12 flimclsi SfJfLimfclsJS
13 12 sselda SfAJfLimfAclsJS
14 13 rexlimivw fFilXSfAJfLimfAclsJS
15 11 14 impbid1 JTopOnXSXAclsJSfFilXSfAJfLimf