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 ‘ 𝐶 ) )