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	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \to (F \in (J CnP K) (A) \leftrightarrow (F : X ⟶ Y \land \forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F))))$

Proof

Step	Hyp	Ref	Expression
1		cnpf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J CnP K) (A)) \to F : X ⟶ Y$
2	1	3expa	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J CnP K) (A)) \to F : X ⟶ Y$
3	2	3adantl3	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F \in (J CnP K) (A)) \to F : X ⟶ Y$
4		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
5		cnpfcfi	$⊢ (K \in Top \land A \in (J fClus f) \land F \in (J CnP K) (A)) \to F (A) \in (K fClusf f) (F)$
6	5	3com23	$⊢ (K \in Top \land F \in (J CnP K) (A) \land A \in (J fClus f)) \to F (A) \in (K fClusf f) (F)$
7	6	3expia	$⊢ (K \in Top \land F \in (J CnP K) (A)) \to (A \in (J fClus f) \to F (A) \in (K fClusf f) (F))$
8	4 7	sylan	$⊢ (K \in TopOn (Y) \land F \in (J CnP K) (A)) \to (A \in (J fClus f) \to F (A) \in (K fClusf f) (F))$
9	8	ralrimivw	$⊢ (K \in TopOn (Y) \land F \in (J CnP K) (A)) \to \forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F))$
10	9	3ad2antl2	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F \in (J CnP K) (A)) \to \forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F))$
11	3 10	jca	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F \in (J CnP K) (A)) \to (F : X ⟶ Y \land \forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)))$
12	11	ex	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \to (F \in (J CnP K) (A) \to (F : X ⟶ Y \land \forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F))))$
13		simplrl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \to g \in Fil (X)$
14		filfbas	$⊢ g \in Fil (X) \to g \in fBas (X)$
15	13 14	syl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \to g \in fBas (X)$
16		simprl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \to h \in Fil (Y)$
17		simpllr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \to F : X ⟶ Y$
18		simprr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \to (Y FilMap F) (g) \subseteq h$
19	15 16 17 18	fmfnfm	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \to \exists f \in Fil (X) (g \subseteq f \land h = (Y FilMap F) (f))$
20		r19.29	$⊢ (\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \land \exists f \in Fil (X) (g \subseteq f \land h = (Y FilMap F) (f))) \to \exists f \in Fil (X) ((A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \land (g \subseteq f \land h = (Y FilMap F) (f)))$
21		flimfcls	$⊢ J fLim f \subseteq J fClus f$
22		simpll1	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to J \in TopOn (X)$
23	22	ad2antrr	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to J \in TopOn (X)$
24		simprl	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to f \in Fil (X)$
25		simprrl	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to g \subseteq f$
26		flimss2	$⊢ (J \in TopOn (X) \land f \in Fil (X) \land g \subseteq f) \to J fLim g \subseteq J fLim f$
27	23 24 25 26	syl3anc	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to J fLim g \subseteq J fLim f$
28		simprr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to A \in (J fLim g)$
29	28	ad2antrr	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to A \in (J fLim g)$
30	27 29	sseldd	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to A \in (J fLim f)$
31	21 30	sseldi	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to A \in (J fClus f)$
32		simpll2	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to K \in TopOn (Y)$
33	32	ad2antrr	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to K \in TopOn (Y)$
34		simplr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to F : X ⟶ Y$
35	34	ad2antrr	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to F : X ⟶ Y$
36		fcfval	$⊢ (K \in TopOn (Y) \land f \in Fil (X) \land F : X ⟶ Y) \to (K fClusf f) (F) = K fClus (Y FilMap F) (f)$
37	33 24 35 36	syl3anc	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to (K fClusf f) (F) = K fClus (Y FilMap F) (f)$
38		simprrr	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to h = (Y FilMap F) (f)$
39	38	oveq2d	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to K fClus h = K fClus (Y FilMap F) (f)$
40	37 39	eqtr4d	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to (K fClusf f) (F) = K fClus h$
41	40	eleq2d	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to (F (A) \in (K fClusf f) (F) \leftrightarrow F (A) \in (K fClus h))$
42	41	biimpd	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to (F (A) \in (K fClusf f) (F) \to F (A) \in (K fClus h))$
43	31 42	embantd	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land (f \in Fil (X) \land (g \subseteq f \land h = (Y FilMap F) (f)))) \to ((A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to F (A) \in (K fClus h))$
44	43	expr	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land f \in Fil (X)) \to ((g \subseteq f \land h = (Y FilMap F) (f)) \to ((A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to F (A) \in (K fClus h)))$
45	44	impcomd	$⊢ (((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \land f \in Fil (X)) \to (((A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \land (g \subseteq f \land h = (Y FilMap F) (f))) \to F (A) \in (K fClus h))$
46	45	rexlimdva	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \to (\exists f \in Fil (X) ((A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \land (g \subseteq f \land h = (Y FilMap F) (f))) \to F (A) \in (K fClus h))$
47	20 46	syl5	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \to ((\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \land \exists f \in Fil (X) (g \subseteq f \land h = (Y FilMap F) (f))) \to F (A) \in (K fClus h))$
48	19 47	mpan2d	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land (h \in Fil (Y) \land (Y FilMap F) (g) \subseteq h)) \to (\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to F (A) \in (K fClus h))$
49	48	expr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land h \in Fil (Y)) \to ((Y FilMap F) (g) \subseteq h \to (\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to F (A) \in (K fClus h)))$
50	49	com23	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \land h \in Fil (Y)) \to (\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to ((Y FilMap F) (g) \subseteq h \to F (A) \in (K fClus h)))$
51	50	ralrimdva	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to (\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to \forall h \in Fil (Y) ((Y FilMap F) (g) \subseteq h \to F (A) \in (K fClus h)))$
52		toponmax	$⊢ K \in TopOn (Y) \to Y \in K$
53	32 52	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to Y \in K$
54		simprl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to g \in Fil (X)$
55	54 14	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to g \in fBas (X)$
56		fmfil	$⊢ (Y \in K \land g \in fBas (X) \land F : X ⟶ Y) \to (Y FilMap F) (g) \in Fil (Y)$
57	53 55 34 56	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to (Y FilMap F) (g) \in Fil (Y)$
58		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
59	32 58	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to Y = ⋃ K$
60	59	fveq2d	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to Fil (Y) = Fil (⋃ K)$
61	57 60	eleqtrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to (Y FilMap F) (g) \in Fil (⋃ K)$
62		eqid	$⊢ ⋃ K = ⋃ K$
63	62	flimfnfcls	$⊢ (Y FilMap F) (g) \in Fil (⋃ K) \to (F (A) \in (K fLim (Y FilMap F) (g)) \leftrightarrow \forall h \in Fil (⋃ K) ((Y FilMap F) (g) \subseteq h \to F (A) \in (K fClus h)))$
64	61 63	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to (F (A) \in (K fLim (Y FilMap F) (g)) \leftrightarrow \forall h \in Fil (⋃ K) ((Y FilMap F) (g) \subseteq h \to F (A) \in (K fClus h)))$
65		flfval	$⊢ (K \in TopOn (Y) \land g \in Fil (X) \land F : X ⟶ Y) \to (K fLimf g) (F) = K fLim (Y FilMap F) (g)$
66	32 54 34 65	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to (K fLimf g) (F) = K fLim (Y FilMap F) (g)$
67	66	eleq2d	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to (F (A) \in (K fLimf g) (F) \leftrightarrow F (A) \in (K fLim (Y FilMap F) (g)))$
68	60	raleqdv	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to (\forall h \in Fil (Y) ((Y FilMap F) (g) \subseteq h \to F (A) \in (K fClus h)) \leftrightarrow \forall h \in Fil (⋃ K) ((Y FilMap F) (g) \subseteq h \to F (A) \in (K fClus h)))$
69	64 67 68	3bitr4d	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to (F (A) \in (K fLimf g) (F) \leftrightarrow \forall h \in Fil (Y) ((Y FilMap F) (g) \subseteq h \to F (A) \in (K fClus h)))$
70	51 69	sylibrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land (g \in Fil (X) \land A \in (J fLim g))) \to (\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to F (A) \in (K fLimf g) (F))$
71	70	expr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land g \in Fil (X)) \to (A \in (J fLim g) \to (\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to F (A) \in (K fLimf g) (F)))$
72	71	com23	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \land g \in Fil (X)) \to (\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to (A \in (J fLim g) \to F (A) \in (K fLimf g) (F)))$
73	72	ralrimdva	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to (\forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F)) \to \forall g \in Fil (X) (A \in (J fLim g) \to F (A) \in (K fLimf g) (F)))$
74	73	imdistanda	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \to ((F : X ⟶ Y \land \forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F))) \to (F : X ⟶ Y \land \forall g \in Fil (X) (A \in (J fLim g) \to F (A) \in (K fLimf g) (F))))$
75		cnpflf	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \to (F \in (J CnP K) (A) \leftrightarrow (F : X ⟶ Y \land \forall g \in Fil (X) (A \in (J fLim g) \to F (A) \in (K fLimf g) (F))))$
76	74 75	sylibrd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \to ((F : X ⟶ Y \land \forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F))) \to F \in (J CnP K) (A))$
77	12 76	impbid	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \to (F \in (J CnP K) (A) \leftrightarrow (F : X ⟶ Y \land \forall f \in Fil (X) (A \in (J fClus f) \to F (A) \in (K fClusf f) (F))))$

Metamath Proof Explorer

Theorem cnpfcf

Proof