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