Metamath Proof Explorer

Theorem cnpfcfi

Description: Lemma for cnpfcf . If a function is continuous at a point, it respects clustering there. (Contributed by Jeff Hankins, 20-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion cnpfcfi ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A → F ⁡ A ∈ K fClusf L ⁡ F

Proof

Step Hyp Ref Expression
1 simp2 ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A → A ∈ J fClus L
2 eqid ⊢ ⋃ J = ⋃ J
3 2 fclsfil ⊢ A ∈ J fClus L → L ∈ Fil ⁡ ⋃ J
4 3 3ad2ant2 ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A → L ∈ Fil ⁡ ⋃ J
5 fclsfnflim ⊢ L ∈ Fil ⁡ ⋃ J → A ∈ J fClus L ↔ ∃ f ∈ Fil ⁡ ⋃ J L ⊆ f ∧ A ∈ J fLim f
6 4 5 syl ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A → A ∈ J fClus L ↔ ∃ f ∈ Fil ⁡ ⋃ J L ⊆ f ∧ A ∈ J fLim f
7 1 6 mpbid ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A → ∃ f ∈ Fil ⁡ ⋃ J L ⊆ f ∧ A ∈ J fLim f
8 simpl1 ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → K ∈ Top
9 toptopon2 ⊢ K ∈ Top ↔ K ∈ TopOn ⁡ ⋃ K
10 8 9 sylib ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → K ∈ TopOn ⁡ ⋃ K
11 simprl ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → f ∈ Fil ⁡ ⋃ J
12 eqid ⊢ ⋃ K = ⋃ K
13 2 12 cnpf ⊢ F ∈ J CnP K ⁡ A → F : ⋃ J ⟶ ⋃ K
14 13 3ad2ant3 ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A → F : ⋃ J ⟶ ⋃ K
15 14 adantr ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → F : ⋃ J ⟶ ⋃ K
16 flfssfcf ⊢ K ∈ TopOn ⁡ ⋃ K ∧ f ∈ Fil ⁡ ⋃ J ∧ F : ⋃ J ⟶ ⋃ K → K fLimf f ⁡ F ⊆ K fClusf f ⁡ F
17 10 11 15 16 syl3anc ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → K fLimf f ⁡ F ⊆ K fClusf f ⁡ F
18 12 topopn ⊢ K ∈ Top → ⋃ K ∈ K
19 8 18 syl ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → ⋃ K ∈ K
20 4 adantr ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → L ∈ Fil ⁡ ⋃ J
21 filfbas ⊢ L ∈ Fil ⁡ ⋃ J → L ∈ fBas ⁡ ⋃ J
22 20 21 syl ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → L ∈ fBas ⁡ ⋃ J
23 fmfil ⊢ ⋃ K ∈ K ∧ L ∈ fBas ⁡ ⋃ J ∧ F : ⋃ J ⟶ ⋃ K → ⋃ K FilMap F ⁡ L ∈ Fil ⁡ ⋃ K
24 19 22 15 23 syl3anc ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → ⋃ K FilMap F ⁡ L ∈ Fil ⁡ ⋃ K
25 filfbas ⊢ f ∈ Fil ⁡ ⋃ J → f ∈ fBas ⁡ ⋃ J
26 25 ad2antrl ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → f ∈ fBas ⁡ ⋃ J
27 simprrl ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → L ⊆ f
28 fmss ⊢ ⋃ K ∈ K ∧ L ∈ fBas ⁡ ⋃ J ∧ f ∈ fBas ⁡ ⋃ J ∧ F : ⋃ J ⟶ ⋃ K ∧ L ⊆ f → ⋃ K FilMap F ⁡ L ⊆ ⋃ K FilMap F ⁡ f
29 19 22 26 15 27 28 syl32anc ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → ⋃ K FilMap F ⁡ L ⊆ ⋃ K FilMap F ⁡ f
30 fclsss2 ⊢ K ∈ TopOn ⁡ ⋃ K ∧ ⋃ K FilMap F ⁡ L ∈ Fil ⁡ ⋃ K ∧ ⋃ K FilMap F ⁡ L ⊆ ⋃ K FilMap F ⁡ f → K fClus ⋃ K FilMap F ⁡ f ⊆ K fClus ⋃ K FilMap F ⁡ L
31 10 24 29 30 syl3anc ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → K fClus ⋃ K FilMap F ⁡ f ⊆ K fClus ⋃ K FilMap F ⁡ L
32 fcfval ⊢ K ∈ TopOn ⁡ ⋃ K ∧ f ∈ Fil ⁡ ⋃ J ∧ F : ⋃ J ⟶ ⋃ K → K fClusf f ⁡ F = K fClus ⋃ K FilMap F ⁡ f
33 10 11 15 32 syl3anc ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → K fClusf f ⁡ F = K fClus ⋃ K FilMap F ⁡ f
34 fcfval ⊢ K ∈ TopOn ⁡ ⋃ K ∧ L ∈ Fil ⁡ ⋃ J ∧ F : ⋃ J ⟶ ⋃ K → K fClusf L ⁡ F = K fClus ⋃ K FilMap F ⁡ L
35 10 20 15 34 syl3anc ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → K fClusf L ⁡ F = K fClus ⋃ K FilMap F ⁡ L
36 31 33 35 3sstr4d ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → K fClusf f ⁡ F ⊆ K fClusf L ⁡ F
37 17 36 sstrd ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → K fLimf f ⁡ F ⊆ K fClusf L ⁡ F
38 simprrr ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → A ∈ J fLim f
39 simpl3 ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → F ∈ J CnP K ⁡ A
40 cnpflfi ⊢ A ∈ J fLim f ∧ F ∈ J CnP K ⁡ A → F ⁡ A ∈ K fLimf f ⁡ F
41 38 39 40 syl2anc ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → F ⁡ A ∈ K fLimf f ⁡ F
42 37 41 sseldd ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A ∧ f ∈ Fil ⁡ ⋃ J ∧ L ⊆ f ∧ A ∈ J fLim f → F ⁡ A ∈ K fClusf L ⁡ F
43 7 42 rexlimddv ⊢ K ∈ Top ∧ A ∈ J fClus L ∧ F ∈ J CnP K ⁡ A → F ⁡ A ∈ K fClusf L ⁡ F