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 𝐿 ) ‘ 𝐹 ) )