Metamath Proof Explorer


Theorem flimtopon

Description: Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion flimtopon
|- ( A e. ( J fLim F ) -> ( J e. ( TopOn ` X ) <-> F e. ( Fil ` X ) ) )

Proof

Step Hyp Ref Expression
1 flimtop
 |-  ( A e. ( J fLim F ) -> J e. Top )
2 istopon
 |-  ( J e. ( TopOn ` X ) <-> ( J e. Top /\ X = U. J ) )
3 2 baib
 |-  ( J e. Top -> ( J e. ( TopOn ` X ) <-> X = U. J ) )
4 1 3 syl
 |-  ( A e. ( J fLim F ) -> ( J e. ( TopOn ` X ) <-> X = U. J ) )
5 eqid
 |-  U. J = U. J
6 5 flimfil
 |-  ( A e. ( J fLim F ) -> F e. ( Fil ` U. J ) )
7 fveq2
 |-  ( X = U. J -> ( Fil ` X ) = ( Fil ` U. J ) )
8 7 eleq2d
 |-  ( X = U. J -> ( F e. ( Fil ` X ) <-> F e. ( Fil ` U. J ) ) )
9 6 8 syl5ibrcom
 |-  ( A e. ( J fLim F ) -> ( X = U. J -> F e. ( Fil ` X ) ) )
10 filunibas
 |-  ( F e. ( Fil ` U. J ) -> U. F = U. J )
11 6 10 syl
 |-  ( A e. ( J fLim F ) -> U. F = U. J )
12 filunibas
 |-  ( F e. ( Fil ` X ) -> U. F = X )
13 12 eqeq1d
 |-  ( F e. ( Fil ` X ) -> ( U. F = U. J <-> X = U. J ) )
14 11 13 syl5ibcom
 |-  ( A e. ( J fLim F ) -> ( F e. ( Fil ` X ) -> X = U. J ) )
15 9 14 impbid
 |-  ( A e. ( J fLim F ) -> ( X = U. J <-> F e. ( Fil ` X ) ) )
16 4 15 bitrd
 |-  ( A e. ( J fLim F ) -> ( J e. ( TopOn ` X ) <-> F e. ( Fil ` X ) ) )