Theorem cnpfcf 24307

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

Assertion

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

Distinct variable groups:   𝐴,𝑓   𝑓,𝐹   𝑓,𝐽   𝑓,𝐾   𝑓,𝑋   𝑓,𝑌

Proof of Theorem cnpfcf

Dummy variables 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnpf2 23515	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶𝑌)
2	1	3expa 1136	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶𝑌)
3	2	3adantl3 1187	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶𝑌)
4		topontop 23178	. . . . . . 7 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
5		cnpfcfi 24306	. . . . . . . . 9 ⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝑓) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))
6	5	3com23 1144	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝐴 ∈ (𝐽 fClus 𝑓)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))
7	6	3expia 1139	. . . . . . 7 ⊢ ((𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
8	4, 7	sylan 592	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
9	8	ralrimivw 3158	. . . . 5 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
10	9	3ad2antl2 1205	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
11	3, 10	jca 521	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))
12	11	ex 418	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))
13		simplrl 789	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → 𝑔 ∈ (Fil‘𝑋))
14		filfbas 24114	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ (Fil‘𝑋) → 𝑔 ∈ (fBas‘𝑋))
15	13, 14	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → 𝑔 ∈ (fBas‘𝑋))
16		simprl 783	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ℎ ∈ (Fil‘𝑌))
17		simpllr 788	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → 𝐹:𝑋⟶𝑌)
18		simprr 785	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)
19	15, 16, 17, 18	fmfnfm 24224	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ∃𝑓 ∈ (Fil‘𝑋)(𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))
20		r19.29 3125	. . . . . . . . . . . . 13 ⊢ ((∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ ∃𝑓 ∈ (Fil‘𝑋)(𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → ∃𝑓 ∈ (Fil‘𝑋)((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))))
21		flimfcls 24292	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 fLim 𝑓) ⊆ (𝐽 fClus 𝑓)
22		simpll1 1231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐽 ∈ (TopOn‘𝑋))
23	22	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐽 ∈ (TopOn‘𝑋))
24		simprl 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝑓 ∈ (Fil‘𝑋))
25		simprrl 793	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝑔 ⊆ 𝑓)
26		flimss2 24238	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝑔 ⊆ 𝑓) → (𝐽 fLim 𝑔) ⊆ (𝐽 fLim 𝑓))
27	23, 24, 25, 26	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → (𝐽 fLim 𝑔) ⊆ (𝐽 fLim 𝑓))
28		simprr 785	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐴 ∈ (𝐽 fLim 𝑔))
29	28	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑔))
30	27, 29	sseldd 3932	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑓))
31	21, 30	sselid 3929	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fClus 𝑓))
32		simpll2 1232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐾 ∈ (TopOn‘𝑌))
33	32	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐾 ∈ (TopOn‘𝑌))
34		simplr 781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐹:𝑋⟶𝑌)
35	34	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐹:𝑋⟶𝑌)
36		fcfval 24299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
37	33, 24, 35, 36	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
38		simprrr 794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ℎ = ((𝑌 FilMap 𝐹)‘𝑓))
39	38	oveq2d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → (𝐾 fClus ℎ) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
40	37, 39	eqtr4d 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ℎ))
41	40	eleq2d 2846	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹) ↔ (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
42	41	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
43	31, 42	embantd 60	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
44	43	expr 462	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ 𝑓 ∈ (Fil‘𝑋)) → ((𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)) → ((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
45	44	impcomd 417	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ 𝑓 ∈ (Fil‘𝑋)) → (((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
46	45	rexlimdva 3163	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → (∃𝑓 ∈ (Fil‘𝑋)((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
47	20, 46	syl5 35	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ((∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ ∃𝑓 ∈ (Fil‘𝑋)(𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
48	19, 47	mpan2d 707	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
49	48	expr 462	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ℎ ∈ (Fil‘𝑌)) → (((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
50	49	com23 87	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ℎ ∈ (Fil‘𝑌)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
51	50	ralrimdva 3162	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → ∀ℎ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
52		toponmax 23191	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
53	32, 52	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑌 ∈ 𝐾)
54		simprl 783	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑔 ∈ (Fil‘𝑋))
55	54, 14	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑔 ∈ (fBas‘𝑋))
56		fmfil 24210	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝐾 ∧ 𝑔 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘𝑌))
57	53, 55, 34, 56	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘𝑌))
58		toponuni 23179	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
59	32, 58	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑌 = ∪ 𝐾)
60	59	fveq2d 6878	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (Fil‘𝑌) = (Fil‘∪ 𝐾))
61	57, 60	eleqtrd 2862	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘∪ 𝐾))
62		eqid 2760	. . . . . . . . . . 11 ⊢ ∪ 𝐾 = ∪ 𝐾
63	62	flimfnfcls 24294	. . . . . . . . . 10 ⊢ (((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘∪ 𝐾) → ((𝐹‘𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)) ↔ ∀ℎ ∈ (Fil‘∪ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
64	61, 63	syl 18	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹‘𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)) ↔ ∀ℎ ∈ (Fil‘∪ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
65		flfval 24256	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝐾 fLimf 𝑔)‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)))
66	32, 54, 34, 65	syl3anc 1398	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐾 fLimf 𝑔)‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)))
67	66	eleq2d 2846	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹) ↔ (𝐹‘𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔))))
68	60	raleqdv 3319	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀ℎ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)) ↔ ∀ℎ ∈ (Fil‘∪ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
69	64, 67, 68	3bitr4d 314	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹) ↔ ∀ℎ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
70	51, 69	sylibrd 262	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))
71	70	expr 462	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝑔) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
72	71	com23 87	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ (Fil‘𝑋)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
73	72	ralrimdva 3162	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
74	73	imdistanda 582	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))))
75		cnpflf 24267	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))))
76	74, 75	sylibrd 262	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
77	12, 76	impbid 215	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086   ⊆ wss 3899  ∪ cuni 4867  ⟶wf 6524  ‘cfv 6528  (class class class)co 7409  fBascfbas 21613  Topctop 23158  TopOnctopon 23175   CnP ccnp 23490  Filcfil 24111   FilMap cfm 24199   fLim cflim 24200   fLimf cflf 24201   fClus cfcls 24202   fClusf cfcf 24203

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7862  df-1st 7985  df-2nd 7986  df-1o 8455  df-2o 8456  df-map 8828  df-en 8953  df-fin 8956  df-fi 9381  df-fbas 21622  df-fg 21623  df-top 23159  df-topon 23176  df-cld 23284  df-ntr 23285  df-cls 23286  df-nei 23363  df-cnp 23493  df-fil 24112  df-fm 24204  df-flim 24205  df-flf 24206  df-fcls 24207  df-fcf 24208

This theorem is used by:  cnfcf  24308