Theorem limcflflem

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

	Ref	Expression
Hypotheses	limcflf.f	|- ( ph -> F : A --> CC )
	limcflf.a	|- ( ph -> A C_ CC )
	limcflf.b	|- ( ph -> B e. ( ( limPt ` K ) ` A ) )
	limcflf.k	|- K = ( TopOpen ` CCfld )
	limcflf.c	|- C = ( A \ { B } )
	limcflf.l	|- L = ( ( ( nei ` K ) ` { B } ) |`t C )
Assertion	limcflflem	|- ( ph -> L e. ( Fil ` C ) )

Proof

Step	Hyp	Ref	Expression
1		limcflf.f	|- ( ph -> F : A --> CC )
2		limcflf.a	|- ( ph -> A C_ CC )
3		limcflf.b	|- ( ph -> B e. ( ( limPt ` K ) ` A ) )
4		limcflf.k	|- K = ( TopOpen ` CCfld )
5		limcflf.c	|- C = ( A \ { B } )
6		limcflf.l	|- L = ( ( ( nei ` K ) ` { B } ) |`t C )
7	4	cnfldtop	|- K e. Top
8	4	cnfldtopon	|- K e. ( TopOn ` CC )
9	8	toponunii	|- CC = U. K
10	9	islp	|- ( ( K e. Top /\ A C_ CC ) -> ( B e. ( ( limPt ` K ) ` A ) <-> B e. ( ( cls ` K ) ` ( A \ { B } ) ) ) )
11	7 2 10	sylancr	|- ( ph -> ( B e. ( ( limPt ` K ) ` A ) <-> B e. ( ( cls ` K ) ` ( A \ { B } ) ) ) )
12	3 11	mpbid	|- ( ph -> B e. ( ( cls ` K ) ` ( A \ { B } ) ) )
13	5	fveq2i	|- ( ( cls ` K ) ` C ) = ( ( cls ` K ) ` ( A \ { B } ) )
14	12 13	eleqtrrdi	|- ( ph -> B e. ( ( cls ` K ) ` C ) )
15		difss	|- ( A \ { B } ) C_ A
16	5 15	eqsstri	|- C C_ A
17	16 2	sstrid	|- ( ph -> C C_ CC )
18	9	lpss	|- ( ( K e. Top /\ A C_ CC ) -> ( ( limPt ` K ) ` A ) C_ CC )
19	7 2 18	sylancr	|- ( ph -> ( ( limPt ` K ) ` A ) C_ CC )
20	19 3	sseldd	|- ( ph -> B e. CC )
21		trnei	|- ( ( K e. ( TopOn ` CC ) /\ C C_ CC /\ B e. CC ) -> ( B e. ( ( cls ` K ) ` C ) <-> ( ( ( nei ` K ) ` { B } ) |`t C ) e. ( Fil ` C ) ) )
22	8 17 20 21	mp3an2i	|- ( ph -> ( B e. ( ( cls ` K ) ` C ) <-> ( ( ( nei ` K ) ` { B } ) |`t C ) e. ( Fil ` C ) ) )
23	14 22	mpbid	|- ( ph -> ( ( ( nei ` K ) ` { B } ) |`t C ) e. ( Fil ` C ) )
24	6 23	eqeltrid	|- ( ph -> L e. ( Fil ` C ) )