Description: A limit point of a filter belongs to its base set. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Mario Carneiro, 9-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | flimuni.1 | |- X = U. J |
|
Assertion | flimelbas | |- ( A e. ( J fLim F ) -> A e. X ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flimuni.1 | |- X = U. J |
|
2 | 1 | elflim2 | |- ( A e. ( J fLim F ) <-> ( ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P X ) /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) ) |
3 | 2 | simprbi | |- ( A e. ( J fLim F ) -> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) |
4 | 3 | simpld | |- ( A e. ( J fLim F ) -> A e. X ) |