cnpflf

Description: Continuity of a function at a point in terms of filter limits. (Contributed by Jeff Hankins, 7-Sep-2009) (Revised by Stefan O'Rear, 7-Aug-2015)

		Ref	Expression
	Assertion	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 f \in Fil (X) (A \in (J fLim f) \to F (A) \in (K fLimf 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		cnpflfi	$⊢ (A \in (J fLim f) \land F \in (J CnP K) (A)) \to F (A) \in (K fLimf f) (F)$
5	4	expcom	$⊢ F \in (J CnP K) (A) \to (A \in (J fLim f) \to F (A) \in (K fLimf f) (F))$
6	5	ralrimivw	$⊢ F \in (J CnP K) (A) \to \forall f \in Fil (X) (A \in (J fLim f) \to F (A) \in (K fLimf f) (F))$
7	6	adantl	$⊢ ((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 fLim f) \to F (A) \in (K fLimf f) (F))$
8	3 7	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 fLim f) \to F (A) \in (K fLimf f) (F)))$
9	8	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 fLim f) \to F (A) \in (K fLimf f) (F))))$
10		simpl1	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to J \in TopOn (X)$
11		simpl3	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to A \in X$
12		neiflim	$⊢ (J \in TopOn (X) \land A \in X) \to A \in (J fLim nei (J) (\{A\}))$
13	10 11 12	syl2anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to A \in (J fLim nei (J) (\{A\}))$
14	11	snssd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to \{A\} \subseteq X$
15		snnzg	$⊢ A \in X \to \{A\} \neq \emptyset$
16	11 15	syl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to \{A\} \neq \emptyset$
17		neifil	$⊢ (J \in TopOn (X) \land \{A\} \subseteq X \land \{A\} \neq \emptyset) \to nei (J) (\{A\}) \in Fil (X)$
18	10 14 16 17	syl3anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to nei (J) (\{A\}) \in Fil (X)$
19		oveq2	$⊢ f = nei (J) (\{A\}) \to J fLim f = J fLim nei (J) (\{A\})$
20	19	eleq2d	$⊢ f = nei (J) (\{A\}) \to (A \in (J fLim f) \leftrightarrow A \in (J fLim nei (J) (\{A\})))$
21		oveq2	$⊢ f = nei (J) (\{A\}) \to K fLimf f = K fLimf nei (J) (\{A\})$
22	21	fveq1d	$⊢ f = nei (J) (\{A\}) \to (K fLimf f) (F) = (K fLimf nei (J) (\{A\})) (F)$
23	22	eleq2d	$⊢ f = nei (J) (\{A\}) \to (F (A) \in (K fLimf f) (F) \leftrightarrow F (A) \in (K fLimf nei (J) (\{A\})) (F))$
24	20 23	imbi12d	$⊢ f = nei (J) (\{A\}) \to ((A \in (J fLim f) \to F (A) \in (K fLimf f) (F)) \leftrightarrow (A \in (J fLim nei (J) (\{A\})) \to F (A) \in (K fLimf nei (J) (\{A\})) (F)))$
25	24	rspcv	$⊢ nei (J) (\{A\}) \in Fil (X) \to (\forall f \in Fil (X) (A \in (J fLim f) \to F (A) \in (K fLimf f) (F)) \to (A \in (J fLim nei (J) (\{A\})) \to F (A) \in (K fLimf nei (J) (\{A\})) (F)))$
26	18 25	syl	$⊢ ((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 fLim f) \to F (A) \in (K fLimf f) (F)) \to (A \in (J fLim nei (J) (\{A\})) \to F (A) \in (K fLimf nei (J) (\{A\})) (F)))$
27	13 26	mpid	$⊢ ((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 fLim f) \to F (A) \in (K fLimf f) (F)) \to F (A) \in (K fLimf nei (J) (\{A\})) (F))$
28	27	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 fLim f) \to F (A) \in (K fLimf f) (F))) \to (F : X ⟶ Y \land F (A) \in (K fLimf nei (J) (\{A\})) (F)))$
29		eqid	$⊢ nei (J) (\{A\}) = nei (J) (\{A\})$
30	29	cnpflf2	$⊢ (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 F (A) \in (K fLimf nei (J) (\{A\})) (F)))$
31	28 30	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 fLim f) \to F (A) \in (K fLimf f) (F))) \to F \in (J CnP K) (A))$
32	9 31	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 fLim f) \to F (A) \in (K fLimf f) (F))))$

Metamath Proof Explorer

Theorem cnpflf

Proof