Theorem fcfneii

Description: A neighborhood of a cluster point of a function contains a function value from every tail. (Contributed by Jeff Hankins, 27-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

	Ref	Expression
Assertion	fcfneii	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐿 ) ) → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		fcfnei	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
2		ineq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) = ( 𝑁 ∩ ( 𝐹 “ 𝑠 ) ) )
3	2	neeq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ↔ ( 𝑁 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
4		imaeq2	⊢ ( 𝑠 = 𝑆 → ( 𝐹 “ 𝑠 ) = ( 𝐹 “ 𝑆 ) )
5	4	ineq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑁 ∩ ( 𝐹 “ 𝑠 ) ) = ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) )
6	5	neeq1d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑁 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ↔ ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) )
7	3 6	rspc2v	⊢ ( ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐿 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) )
8	7	ex	⊢ ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑆 ∈ 𝐿 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) ) )
9	8	com3r	⊢ ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑆 ∈ 𝐿 → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) ) )
10	9	adantl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑆 ∈ 𝐿 → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) ) )
11	1 10	biimtrdi	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑆 ∈ 𝐿 → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ ) ) ) )
12	11	3imp2	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐿 ) ) → ( 𝑁 ∩ ( 𝐹 “ 𝑆 ) ) ≠ ∅ )