Metamath Proof Explorer

Theorem cnpfcf

Description: A function F is continuous at point A iff F respects cluster points there. (Contributed by Jeff Hankins, 14-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion cnpfcf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
2 1 3expa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
3 2 3adantl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
4 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
5 cnpfcfi ⊢ ( ( 𝐾 ∈ Top ∧ 𝐴 ∈ ( 𝐽 fClus 𝑓 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) )
6 5 3com23 ⊢ ( ( 𝐾 ∈ Top ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝐴 ∈ ( 𝐽 fClus 𝑓 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) )
7 6 3expia ⊢ ( ( 𝐾 ∈ Top ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) )
8 4 7 sylan ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) )
9 8 ralrimivw ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) )
10 9 3ad2antl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) )
11 3 10 jca ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )
12 11 ex ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) )
13 simplrl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) → 𝑔 ∈ ( Fil ‘ 𝑋 ) )
14 filfbas ⊢ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) → 𝑔 ∈ ( fBas ‘ 𝑋 ) )
15 13 14 syl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) → 𝑔 ∈ ( fBas ‘ 𝑋 ) )
16 simprl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) → ℎ ∈ ( Fil ‘ 𝑌 ) )
17 simpllr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
18 simprr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) → ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ )
19 15 16 17 18 fmfnfm ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) )
20 r19.29 ⊢ ( ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ∧ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) )
21 flimfcls ⊢ ( 𝐽 fLim 𝑓 ) ⊆ ( 𝐽 fClus 𝑓 )
22 simpll1 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
23 22 ad2antrr ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
24 simprl ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
25 simprrl ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → 𝑔 ⊆ 𝑓 )
26 flimss2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ⊆ 𝑓 ) → ( 𝐽 fLim 𝑔 ) ⊆ ( 𝐽 fLim 𝑓 ) )
27 23 24 25 26 syl3anc ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → ( 𝐽 fLim 𝑔 ) ⊆ ( 𝐽 fLim 𝑓 ) )
28 simprr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → 𝐴 ∈ ( 𝐽 fLim 𝑔 ) )
29 28 ad2antrr ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → 𝐴 ∈ ( 𝐽 fLim 𝑔 ) )
30 27 29 sseldd ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → 𝐴 ∈ ( 𝐽 fLim 𝑓 ) )
31 21 30 sselid ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → 𝐴 ∈ ( 𝐽 fClus 𝑓 ) )
32 simpll2 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
33 32 ad2antrr ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
34 simplr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
35 34 ad2antrr ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
36 fcfval ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) = ( 𝐾 fClus ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) )
37 33 24 35 36 syl3anc ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) = ( 𝐾 fClus ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) )
38 simprrr ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) )
39 38 oveq2d ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → ( 𝐾 fClus ℎ ) = ( 𝐾 fClus ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) )
40 37 39 eqtr4d ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) = ( 𝐾 fClus ℎ ) )
41 40 eleq2d ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) )
42 41 biimpd ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) )
43 31 42 embantd ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) ) → ( ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) )
44 43 expr ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) → ( ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) ) )
45 44 impcomd ⊢ ( ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( ( ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) )
46 45 rexlimdva ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) → ( ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ∧ ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) )
47 20 46 syl5 ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) → ( ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ∧ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑔 ⊆ 𝑓 ∧ ℎ = ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑓 ) ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) )
48 19 47 mpan2d ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ( ℎ ∈ ( Fil ‘ 𝑌 ) ∧ ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ ) ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) )
49 48 expr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ℎ ∈ ( Fil ‘ 𝑌 ) ) → ( ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) ) )
50 49 com23 ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) ∧ ℎ ∈ ( Fil ‘ 𝑌 ) ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ( ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) ) )
51 50 ralrimdva ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ∀ ℎ ∈ ( Fil ‘ 𝑌 ) ( ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) ) )
52 toponmax ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 ∈ 𝐾 )
53 32 52 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → 𝑌 ∈ 𝐾 )
54 simprl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → 𝑔 ∈ ( Fil ‘ 𝑋 ) )
55 54 14 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → 𝑔 ∈ ( fBas ‘ 𝑋 ) )
56 fmfil ⊢ ( ( 𝑌 ∈ 𝐾 ∧ 𝑔 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ∈ ( Fil ‘ 𝑌 ) )
57 53 55 34 56 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ∈ ( Fil ‘ 𝑌 ) )
58 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
59 32 58 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → 𝑌 = ∪ 𝐾 )
60 59 fveq2d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( Fil ‘ 𝑌 ) = ( Fil ‘ ∪ 𝐾 ) )
61 57 60 eleqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ∈ ( Fil ‘ ∪ 𝐾 ) )
62 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
63 62 flimfnfcls ⊢ ( ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ∈ ( Fil ‘ ∪ 𝐾 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ) ↔ ∀ ℎ ∈ ( Fil ‘ ∪ 𝐾 ) ( ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) ) )
64 61 63 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ) ↔ ∀ ℎ ∈ ( Fil ‘ ∪ 𝐾 ) ( ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) ) )
65 flfval ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ) )
66 32 54 34 65 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ) )
67 66 eleq2d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ) ) )
68 60 raleqdv ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( ∀ ℎ ∈ ( Fil ‘ 𝑌 ) ( ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) ↔ ∀ ℎ ∈ ( Fil ‘ ∪ 𝐾 ) ( ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) ) )
69 64 67 68 3bitr4d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) ↔ ∀ ℎ ∈ ( Fil ‘ 𝑌 ) ( ( ( 𝑌 FilMap 𝐹 ) ‘ 𝑔 ) ⊆ ℎ → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐾 fClus ℎ ) ) ) )
70 51 69 sylibrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ ( 𝐽 fLim 𝑔 ) ) ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) ) )
71 70 expr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝑔 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) ) ) )
72 71 com23 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝑔 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) ) ) )
73 72 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) → ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑔 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) ) ) )
74 73 imdistanda ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑔 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) ) ) ) )
75 cnpflf ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑔 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑔 ) ‘ 𝐹 ) ) ) ) )
76 74 75 sylibrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) )
77 12 76 impbid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) )