Theorem flfnei

Description: The property of being a limit point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 9-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

	Ref	Expression
Assertion	flfnei	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flfval	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
2	1	eleq2d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ 𝐴 ∈ ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) )
3		simp1	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4		toponmax	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
5	4	3ad2ant1	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑋 ∈ 𝐽 )
6		filfbas	⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
7	6	3ad2ant2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
8		simp3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐹 : 𝑌 ⟶ 𝑋 )
9		fmfil	⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
10	5 7 8 9	syl3anc	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
11		elflim	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) )
12	3 10 11	syl2anc	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) )
13		dfss3	⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑛 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )
14		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
15	14	3ad2ant1	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐽 ∈ Top )
16		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
17	16	neii1	⊢ ( ( 𝐽 ∈ Top ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑛 ⊆ ∪ 𝐽 )
18	15 17	sylan	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑛 ⊆ ∪ 𝐽 )
19		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
20	19	3ad2ant1	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑋 = ∪ 𝐽 )
21	20	adantr	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑋 = ∪ 𝐽 )
22	18 21	sseqtrrd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑛 ⊆ 𝑋 )
23		elfm	⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑛 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑛 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) ) )
24	5 7 8 23	syl3anc	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑛 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑛 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) ) )
25	24	baibd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑛 ⊆ 𝑋 ) → ( 𝑛 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) )
26	22 25	syldan	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝑛 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) )
27	26	ralbidva	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑛 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) )
28	13 27	syl5bb	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) )
29	28	anbi2d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) ) )
30	2 12 29	3bitrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) ) )