Theorem cnpfcf 22333

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 21542	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶𝑌)
2	1	3expa 1111	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶𝑌)
3	2	3adantl3 1161	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶𝑌)
4		topontop 21205	. . . . . . 7 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
5		cnpfcfi 22332	. . . . . . . . 9 ⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝑓) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))
6	5	3com23 1119	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝐴 ∈ (𝐽 fClus 𝑓)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))
7	6	3expia 1114	. . . . . . 7 ⊢ ((𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
8	4, 7	sylan 580	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
9	8	ralrimivw 3150	. . . . 5 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
10	9	3ad2antl2 1179	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
11	3, 10	jca 512	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))
12	11	ex 413	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))
13		simplrl 773	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → 𝑔 ∈ (Fil‘𝑋))
14		filfbas 22140	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ (Fil‘𝑋) → 𝑔 ∈ (fBas‘𝑋))
15	13, 14	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → 𝑔 ∈ (fBas‘𝑋))
16		simprl 767	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ℎ ∈ (Fil‘𝑌))
17		simpllr 772	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → 𝐹:𝑋⟶𝑌)
18		simprr 769	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)
19	15, 16, 17, 18	fmfnfm 22250	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ∃𝑓 ∈ (Fil‘𝑋)(𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))
20		r19.29 3218	. . . . . . . . . . . . 13 ⊢ ((∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ ∃𝑓 ∈ (Fil‘𝑋)(𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → ∃𝑓 ∈ (Fil‘𝑋)((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))))
21		flimfcls 22318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 fLim 𝑓) ⊆ (𝐽 fClus 𝑓)
22		simpll1 1205	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐽 ∈ (TopOn‘𝑋))
23	22	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐽 ∈ (TopOn‘𝑋))
24		simprl 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝑓 ∈ (Fil‘𝑋))
25		simprrl 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝑔 ⊆ 𝑓)
26		flimss2 22264	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝑔 ⊆ 𝑓) → (𝐽 fLim 𝑔) ⊆ (𝐽 fLim 𝑓))
27	23, 24, 25, 26	syl3anc 1364	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → (𝐽 fLim 𝑔) ⊆ (𝐽 fLim 𝑓))
28		simprr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐴 ∈ (𝐽 fLim 𝑔))
29	28	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑔))
30	27, 29	sseldd 3890	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑓))
31	21, 30	sseldi 3887	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fClus 𝑓))
32		simpll2 1206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐾 ∈ (TopOn‘𝑌))
33	32	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐾 ∈ (TopOn‘𝑌))
34		simplr 765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐹:𝑋⟶𝑌)
35	34	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐹:𝑋⟶𝑌)
36		fcfval 22325	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
37	33, 24, 35, 36	syl3anc 1364	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
38		simprrr 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ℎ = ((𝑌 FilMap 𝐹)‘𝑓))
39	38	oveq2d 7032	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → (𝐾 fClus ℎ) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
40	37, 39	eqtr4d 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ℎ))
41	40	eleq2d 2868	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹) ↔ (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
42	41	biimpd 230	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
43	31, 42	embantd 59	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
44	43	expr 457	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ 𝑓 ∈ (Fil‘𝑋)) → ((𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)) → ((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
45	44	impcomd 412	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ 𝑓 ∈ (Fil‘𝑋)) → (((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
46	45	rexlimdva 3247	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → (∃𝑓 ∈ (Fil‘𝑋)((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
47	20, 46	syl5 34	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ((∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ ∃𝑓 ∈ (Fil‘𝑋)(𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
48	19, 47	mpan2d 690	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
49	48	expr 457	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ℎ ∈ (Fil‘𝑌)) → (((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
50	49	com23 86	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ℎ ∈ (Fil‘𝑌)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
51	50	ralrimdva 3156	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → ∀ℎ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
52		toponmax 21218	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
53	32, 52	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑌 ∈ 𝐾)
54		simprl 767	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑔 ∈ (Fil‘𝑋))
55	54, 14	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑔 ∈ (fBas‘𝑋))
56		fmfil 22236	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝐾 ∧ 𝑔 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘𝑌))
57	53, 55, 34, 56	syl3anc 1364	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘𝑌))
58		toponuni 21206	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
59	32, 58	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑌 = ∪ 𝐾)
60	59	fveq2d 6542	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (Fil‘𝑌) = (Fil‘∪ 𝐾))
61	57, 60	eleqtrd 2885	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘∪ 𝐾))
62		eqid 2795	. . . . . . . . . . 11 ⊢ ∪ 𝐾 = ∪ 𝐾
63	62	flimfnfcls 22320	. . . . . . . . . 10 ⊢ (((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘∪ 𝐾) → ((𝐹‘𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)) ↔ ∀ℎ ∈ (Fil‘∪ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
64	61, 63	syl 17	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹‘𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)) ↔ ∀ℎ ∈ (Fil‘∪ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
65		flfval 22282	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝐾 fLimf 𝑔)‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)))
66	32, 54, 34, 65	syl3anc 1364	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐾 fLimf 𝑔)‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)))
67	66	eleq2d 2868	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹) ↔ (𝐹‘𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔))))
68	60	raleqdv 3375	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀ℎ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)) ↔ ∀ℎ ∈ (Fil‘∪ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
69	64, 67, 68	3bitr4d 312	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹) ↔ ∀ℎ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
70	51, 69	sylibrd 260	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))
71	70	expr 457	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝑔) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
72	71	com23 86	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ (Fil‘𝑋)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
73	72	ralrimdva 3156	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
74	73	imdistanda 572	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))))
75		cnpflf 22293	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))))
76	74, 75	sylibrd 260	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
77	12, 76	impbid 213	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1522   ∈ wcel 2081  ∀wral 3105  ∃wrex 3106   ⊆ wss 3859  ∪ cuni 4745  ⟶wf 6221  ‘cfv 6225  (class class class)co 7016  fBascfbas 20215  Topctop 21185  TopOnctopon 21202   CnP ccnp 21517  Filcfil 22137   FilMap cfm 22225   fLim cflim 22226   fLimf cflf 22227   fClus cfcls 22228   fClusf cfcf 22229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-map 8258  df-en 8358  df-fin 8361  df-fi 8721  df-fbas 20224  df-fg 20225  df-top 21186  df-topon 21203  df-cld 21311  df-ntr 21312  df-cls 21313  df-nei 21390  df-cnp 21520  df-fil 22138  df-fm 22230  df-flim 22231  df-flf 22232  df-fcls 22233  df-fcf 22234

This theorem is referenced by:  cnfcf  22334