Metamath Proof Explorer
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 |
⊢ 𝑋 = ∪ 𝐽 |
|
Assertion |
flimelbas |
⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐴 ∈ 𝑋 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
flimuni.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
1
|
elflim2 |
⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) ) |
3 |
2
|
simprbi |
⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) |
4 |
3
|
simpld |
⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐴 ∈ 𝑋 ) |