Metamath Proof Explorer


Theorem isfcls2

Description: A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion isfcls2 JTopOnXFFilXAJfClusFsFAclsJs

Proof

Step Hyp Ref Expression
1 topontop JTopOnXJTop
2 toponuni JTopOnXX=J
3 2 fveq2d JTopOnXFilX=FilJ
4 3 eleq2d JTopOnXFFilXFFilJ
5 4 biimpa JTopOnXFFilXFFilJ
6 eqid J=J
7 6 isfcls AJfClusFJTopFFilJsFAclsJs
8 df-3an JTopFFilJsFAclsJsJTopFFilJsFAclsJs
9 7 8 bitri AJfClusFJTopFFilJsFAclsJs
10 9 baib JTopFFilJAJfClusFsFAclsJs
11 1 5 10 syl2an2r JTopOnXFFilXAJfClusFsFAclsJs