Description: Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fclstop | |- ( A e. ( J fClus F ) -> J e. Top ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |- U. J = U. J |
|
2 | 1 | isfcls | |- ( A e. ( J fClus F ) <-> ( J e. Top /\ F e. ( Fil ` U. J ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) ) |
3 | 2 | simp1bi | |- ( A e. ( J fClus F ) -> J e. Top ) |