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 ( ( 𝐾 ∈ Top ∧ 𝐴 ∈ ( 𝐽 fClus 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fClusf 𝐿 ) ‘ 𝐹 ) )

Proof

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