Theorem flfneii

Description: A neighborhood of a limit point of a function contains the image of a filter element. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

	Ref	Expression
Hypothesis	flfneii.x	⊢ 𝑋 = ∪ 𝐽
Assertion	flfneii	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		flfneii.x	⊢ 𝑋 = ∪ 𝐽
2	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		flfnei	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) ) )
4	2 3	syl3an1b	⊢ ( ( 𝐽 ∈ Top ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ) ) )
5	4	simplbda	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ) → ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 )
6	5	3adant3	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 )
7		sseq2	⊢ ( 𝑛 = 𝑁 → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ↔ ( 𝐹 “ 𝑠 ) ⊆ 𝑁 ) )
8	7	rexbidv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 ↔ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑁 ) )
9	8	rspcv	⊢ ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑁 ) )
10	9	3ad2ant3	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑛 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑁 ) )
11	6 10	mpd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑁 )