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	11	snn0d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to \{A\} \neq \emptyset$
16		neifil	$⊢ (J \in TopOn (X) \land \{A\} \subseteq X \land \{A\} \neq \emptyset) \to nei (J) (\{A\}) \in Fil (X)$
17	10 14 15 16	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)$
18		oveq2	$⊢ f = nei (J) (\{A\}) \to J fLim f = J fLim nei (J) (\{A\})$
19	18	eleq2d	$⊢ f = nei (J) (\{A\}) \to (A \in (J fLim f) \leftrightarrow A \in (J fLim nei (J) (\{A\})))$
20		oveq2	$⊢ f = nei (J) (\{A\}) \to K fLimf f = K fLimf nei (J) (\{A\})$
21	20	fveq1d	$⊢ f = nei (J) (\{A\}) \to (K fLimf f) (F) = (K fLimf nei (J) (\{A\})) (F)$
22	21	eleq2d	$⊢ f = nei (J) (\{A\}) \to (F (A) \in (K fLimf f) (F) \leftrightarrow F (A) \in (K fLimf nei (J) (\{A\})) (F))$
23	19 22	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)))$
24	23	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)))$
25	17 24	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)))$
26	13 25	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))$
27	26	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)))$
28		eqid	$⊢ nei (J) (\{A\}) = nei (J) (\{A\})$
29	28	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)))$
30	27 29	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))$
31	9 30	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