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 J TopOn X S X A cls J S f Fil X S f A J fLim f

Proof

Step Hyp Ref Expression
1 eqid X filGen fi nei J A S = X filGen fi nei J A S
2 1 flimclslem J TopOn X S X A cls J S X filGen fi nei J A S Fil X S X filGen fi nei J A S A J fLim X filGen fi nei J A S
3 3anass X filGen fi nei J A S Fil X S X filGen fi nei J A S A J fLim X filGen fi nei J A S X filGen fi nei J A S Fil X S X filGen fi nei J A S A J fLim X filGen fi nei J A S
4 2 3 sylib J TopOn X S X A cls J S X filGen fi nei J A S Fil X S X filGen fi nei J A S A J fLim X filGen fi nei J A S
5 eleq2 f = X filGen fi nei J A S S f S X filGen fi nei J A S
6 oveq2 f = X filGen fi nei J A S J fLim f = J fLim X filGen fi nei J A S
7 6 eleq2d f = X filGen fi nei J A S A J fLim f A J fLim X filGen fi nei J A S
8 5 7 anbi12d f = X filGen fi nei J A S S f A J fLim f S X filGen fi nei J A S A J fLim X filGen fi nei J A S
9 8 rspcev X filGen fi nei J A S Fil X S X filGen fi nei J A S A J fLim X filGen fi nei J A S f Fil X S f A J fLim f
10 4 9 syl J TopOn X S X A cls J S f Fil X S f A J fLim f
11 10 3expia J TopOn X S X A cls J S f Fil X S f A J fLim f
12 flimclsi S f J fLim f cls J S
13 12 sselda S f A J fLim f A cls J S
14 13 rexlimivw f Fil X S f A J fLim f A cls J S
15 11 14 impbid1 J TopOn X S X A cls J S f Fil X S f A J fLim f