This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limcflflem

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

Ref Expression
Hypotheses limcflf.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limcflf.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
limcflf.b ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
limcflf.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limcflf.c ⊢ 𝐶 = ( 𝐴 ∖ { 𝐵 } )
limcflf.l ⊢ 𝐿 = ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t 𝐶 )
Assertion limcflflem ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 limcflf.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 limcflf.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3 limcflf.b ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
4 limcflf.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
5 limcflf.c ⊢ 𝐶 = ( 𝐴 ∖ { 𝐵 } )
6 limcflf.l ⊢ 𝐿 = ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t 𝐶 )
7 4 cnfldtop ⊢ 𝐾 ∈ Top
8 4 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
9 8 toponunii ⊢ ℂ = ∪ 𝐾
10 9 islp ⊢ ( ( 𝐾 ∈ Top ∧ 𝐴 ⊆ ℂ ) → ( 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) ↔ 𝐵 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) )
11 7 2 10 sylancr ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) ↔ 𝐵 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) )
12 3 11 mpbid ⊢ ( 𝜑 → 𝐵 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) )
13 5 fveq2i ⊢ ( ( cls ‘ 𝐾 ) ‘ 𝐶 ) = ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) )
14 12 13 eleqtrrdi ⊢ ( 𝜑 → 𝐵 ∈ ( ( cls ‘ 𝐾 ) ‘ 𝐶 ) )
15 difss ⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
16 5 15 eqsstri ⊢ 𝐶 ⊆ 𝐴
17 16 2 sstrid ⊢ ( 𝜑 → 𝐶 ⊆ ℂ )
18 9 lpss ⊢ ( ( 𝐾 ∈ Top ∧ 𝐴 ⊆ ℂ ) → ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) ⊆ ℂ )
19 7 2 18 sylancr ⊢ ( 𝜑 → ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) ⊆ ℂ )
20 19 3 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
21 trnei ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐶 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ∈ ( ( cls ‘ 𝐾 ) ‘ 𝐶 ) ↔ ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t 𝐶 ) ∈ ( Fil ‘ 𝐶 ) ) )
22 8 17 20 21 mp3an2i ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( cls ‘ 𝐾 ) ‘ 𝐶 ) ↔ ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t 𝐶 ) ∈ ( Fil ‘ 𝐶 ) ) )
23 14 22 mpbid ⊢ ( 𝜑 → ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t 𝐶 ) ∈ ( Fil ‘ 𝐶 ) )
24 6 23 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝐶 ) )