Theorem isfcf

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

	Ref	Expression
Assertion	isfcf	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fcfval	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
2	1	eleq2d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ 𝐴 ∈ ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) )
3		simp1	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4		toponmax	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
5		filfbas	⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
6		id	⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝐹 : 𝑌 ⟶ 𝑋 )
7		fmfil	⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
8	4 5 6 7	syl3an	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
9		fclsopn	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ) ) )
10	3 8 9	syl2anc	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ) ) )
11		simpll1	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
12	11 4	syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝑋 ∈ 𝐽 )
13		simpll2	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
14	13 5	syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
15		simpll3	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝐹 : 𝑌 ⟶ 𝑋 )
16		simpl2	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
17		fgfil	⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → ( 𝑌 filGen 𝐿 ) = 𝐿 )
18	16 17	syl	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑌 filGen 𝐿 ) = 𝐿 )
19	18	eleq2d	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑠 ∈ ( 𝑌 filGen 𝐿 ) ↔ 𝑠 ∈ 𝐿 ) )
20	19	biimpar	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝑠 ∈ ( 𝑌 filGen 𝐿 ) )
21		eqid	⊢ ( 𝑌 filGen 𝐿 ) = ( 𝑌 filGen 𝐿 )
22	21	imaelfm	⊢ ( ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑠 ∈ ( 𝑌 filGen 𝐿 ) ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )
23	12 14 15 20 22	syl31anc	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )
24		ineq2	⊢ ( 𝑥 = ( 𝐹 “ 𝑠 ) → ( 𝑜 ∩ 𝑥 ) = ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) )
25	24	neeq1d	⊢ ( 𝑥 = ( 𝐹 “ 𝑠 ) → ( ( 𝑜 ∩ 𝑥 ) ≠ ∅ ↔ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
26	25	rspcv	⊢ ( ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) → ( ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ → ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
27	23 26	syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → ( ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ → ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
28	27	ralrimdva	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
29		elfm	⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
30	4 5 6 29	syl3an	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
31	30	adantr	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
32	31	simplbda	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 )
33		r19.29r	⊢ ( ( ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
34		sslin	⊢ ( ( 𝐹 “ 𝑠 ) ⊆ 𝑥 → ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ⊆ ( 𝑜 ∩ 𝑥 ) )
35		ssn0	⊢ ( ( ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ⊆ ( 𝑜 ∩ 𝑥 ) ∧ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑜 ∩ 𝑥 ) ≠ ∅ )
36	34 35	sylan	⊢ ( ( ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑜 ∩ 𝑥 ) ≠ ∅ )
37	36	rexlimivw	⊢ ( ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑜 ∩ 𝑥 ) ≠ ∅ )
38	33 37	syl	⊢ ( ( ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑜 ∩ 𝑥 ) ≠ ∅ )
39	38	ex	⊢ ( ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 → ( ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) )
40	32 39	syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) → ( ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) )
41	40	ralrimdva	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) )
42	28 41	impbid	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
43	42	imbi2d	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ↔ ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
44	43	ralbidva	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
45	44	anbi2d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) ) )
46	2 10 45	3bitrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) ) )