Metamath Proof Explorer

Theorem limcflflem

Description: Lemma for limcflf . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcflf.f ⊢φ→F:A⟶ℂ
limcflf.a ⊢φ→A⊆ℂ
limcflf.b ⊢φ→B∈limPt⁡K⁡A
limcflf.k ⊢K=TopOpen⁡ℂfld
limcflf.c ⊢C=A∖B
limcflf.l ⊢L=nei⁡K⁡B↾𝑡C
Assertion limcflflem ⊢φ→L∈Fil⁡C

Proof

Step Hyp Ref Expression
1 limcflf.f ⊢φ→F:A⟶ℂ
2 limcflf.a ⊢φ→A⊆ℂ
3 limcflf.b ⊢φ→B∈limPt⁡K⁡A
4 limcflf.k ⊢K=TopOpen⁡ℂfld
5 limcflf.c ⊢C=A∖B
6 limcflf.l ⊢L=nei⁡K⁡B↾𝑡C
7 4 cnfldtop ⊢K∈Top
8 4 cnfldtopon ⊢K∈TopOn⁡ℂ
9 8 toponunii ⊢ℂ=⋃K
10 9 islp ⊢K∈Top∧A⊆ℂ→B∈limPt⁡K⁡A↔B∈cls⁡K⁡A∖B
11 7 2 10 sylancr ⊢φ→B∈limPt⁡K⁡A↔B∈cls⁡K⁡A∖B
12 3 11 mpbid ⊢φ→B∈cls⁡K⁡A∖B
13 5 fveq2i ⊢cls⁡K⁡C=cls⁡K⁡A∖B
14 12 13 eleqtrrdi ⊢φ→B∈cls⁡K⁡C
15 difss ⊢A∖B⊆A
16 5 15 eqsstri ⊢C⊆A
17 16 2 sstrid ⊢φ→C⊆ℂ
18 9 lpss ⊢K∈Top∧A⊆ℂ→limPt⁡K⁡A⊆ℂ
19 7 2 18 sylancr ⊢φ→limPt⁡K⁡A⊆ℂ
20 19 3 sseldd ⊢φ→B∈ℂ
21 trnei ⊢K∈TopOn⁡ℂ∧C⊆ℂ∧B∈ℂ→B∈cls⁡K⁡C↔nei⁡K⁡B↾𝑡C∈Fil⁡C
22 8 17 20 21 mp3an2i ⊢φ→B∈cls⁡K⁡C↔nei⁡K⁡B↾𝑡C∈Fil⁡C
23 14 22 mpbid ⊢φ→nei⁡K⁡B↾𝑡C∈Fil⁡C
24 6 23 eqeltrid ⊢φ→L∈Fil⁡C