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	$⊢ (K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \to F (A) \in (K fClusf L) (F)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \to A \in (J fClus L)$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	fclsfil	$⊢ A \in (J fClus L) \to L \in Fil (⋃ J)$
4	3	3ad2ant2	$⊢ (K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \to L \in Fil (⋃ J)$
5		fclsfnflim	$⊢ L \in Fil (⋃ J) \to (A \in (J fClus L) \leftrightarrow \exists f \in Fil (⋃ J) (L \subseteq f \land A \in (J fLim f)))$
6	4 5	syl	$⊢ (K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \to (A \in (J fClus L) \leftrightarrow \exists f \in Fil (⋃ J) (L \subseteq f \land A \in (J fLim f)))$
7	1 6	mpbid	$⊢ (K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \to \exists f \in Fil (⋃ J) (L \subseteq f \land A \in (J fLim f))$
8		simpl1	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to K \in Top$
9		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
10	8 9	sylib	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to K \in TopOn (⋃ K)$
11		simprl	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to f \in Fil (⋃ J)$
12		eqid	$⊢ ⋃ K = ⋃ K$
13	2 12	cnpf	$⊢ F \in (J CnP K) (A) \to F : ⋃ J ⟶ ⋃ K$
14	13	3ad2ant3	$⊢ (K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \to F : ⋃ J ⟶ ⋃ K$
15	14	adantr	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to F : ⋃ J ⟶ ⋃ K$
16		flfssfcf	$⊢ (K \in TopOn (⋃ K) \land f \in Fil (⋃ J) \land F : ⋃ J ⟶ ⋃ K) \to (K fLimf f) (F) \subseteq (K fClusf f) (F)$
17	10 11 15 16	syl3anc	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to (K fLimf f) (F) \subseteq (K fClusf f) (F)$
18	12	topopn	$⊢ K \in Top \to ⋃ K \in K$
19	8 18	syl	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to ⋃ K \in K$
20	4	adantr	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to L \in Fil (⋃ J)$
21		filfbas	$⊢ L \in Fil (⋃ J) \to L \in fBas (⋃ J)$
22	20 21	syl	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to L \in fBas (⋃ J)$
23		fmfil	$⊢ (⋃ K \in K \land L \in fBas (⋃ J) \land F : ⋃ J ⟶ ⋃ K) \to (⋃ K FilMap F) (L) \in Fil (⋃ K)$
24	19 22 15 23	syl3anc	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to (⋃ K FilMap F) (L) \in Fil (⋃ K)$
25		filfbas	$⊢ f \in Fil (⋃ J) \to f \in fBas (⋃ J)$
26	25	ad2antrl	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to f \in fBas (⋃ J)$
27		simprrl	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to L \subseteq f$
28		fmss	$⊢ ((⋃ K \in K \land L \in fBas (⋃ J) \land f \in fBas (⋃ J)) \land (F : ⋃ J ⟶ ⋃ K \land L \subseteq f)) \to (⋃ K FilMap F) (L) \subseteq (⋃ K FilMap F) (f)$
29	19 22 26 15 27 28	syl32anc	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to (⋃ K FilMap F) (L) \subseteq (⋃ K FilMap F) (f)$
30		fclsss2	$⊢ (K \in TopOn (⋃ K) \land (⋃ K FilMap F) (L) \in Fil (⋃ K) \land (⋃ K FilMap F) (L) \subseteq (⋃ K FilMap F) (f)) \to K fClus (⋃ K FilMap F) (f) \subseteq K fClus (⋃ K FilMap F) (L)$
31	10 24 29 30	syl3anc	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to K fClus (⋃ K FilMap F) (f) \subseteq K fClus (⋃ K FilMap F) (L)$
32		fcfval	$⊢ (K \in TopOn (⋃ K) \land f \in Fil (⋃ J) \land F : ⋃ J ⟶ ⋃ K) \to (K fClusf f) (F) = K fClus (⋃ K FilMap F) (f)$
33	10 11 15 32	syl3anc	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to (K fClusf f) (F) = K fClus (⋃ K FilMap F) (f)$
34		fcfval	$⊢ (K \in TopOn (⋃ K) \land L \in Fil (⋃ J) \land F : ⋃ J ⟶ ⋃ K) \to (K fClusf L) (F) = K fClus (⋃ K FilMap F) (L)$
35	10 20 15 34	syl3anc	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to (K fClusf L) (F) = K fClus (⋃ K FilMap F) (L)$
36	31 33 35	3sstr4d	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to (K fClusf f) (F) \subseteq (K fClusf L) (F)$
37	17 36	sstrd	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to (K fLimf f) (F) \subseteq (K fClusf L) (F)$
38		simprrr	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to A \in (J fLim f)$
39		simpl3	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to F \in (J CnP K) (A)$
40		cnpflfi	$⊢ (A \in (J fLim f) \land F \in (J CnP K) (A)) \to F (A) \in (K fLimf f) (F)$
41	38 39 40	syl2anc	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to F (A) \in (K fLimf f) (F)$
42	37 41	sseldd	$⊢ ((K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \land (f \in Fil (⋃ J) \land (L \subseteq f \land A \in (J fLim f)))) \to F (A) \in (K fClusf L) (F)$
43	7 42	rexlimddv	$⊢ (K \in Top \land A \in (J fClus L) \land F \in (J CnP K) (A)) \to F (A) \in (K fClusf L) (F)$

Metamath Proof Explorer

Theorem cnpfcfi

Proof