cnpflf2

Description: F is continuous at point A iff a limit of F when x tends to A is ( FA ) . Proposition 9 of BourbakiTop1 p. TG I.50. (Contributed by FL, 29-May-2011) (Revised by Mario Carneiro, 9-Apr-2015)

		Ref	Expression
	Hypothesis	cnpflf2.3	$⊢ L = nei (J) (\{A\})$
	Assertion	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 L) (F)))$

Proof

Step	Hyp	Ref	Expression
1		cnpflf2.3	$⊢ L = nei (J) (\{A\})$
2		cnpf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J CnP K) (A)) \to F : X ⟶ Y$
3	2	3expa	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J CnP K) (A)) \to F : X ⟶ Y$
4	3	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$
5		simpl1	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F \in (J CnP K) (A)) \to J \in TopOn (X)$
6		simpl3	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F \in (J CnP K) (A)) \to A \in X$
7		neiflim	$⊢ (J \in TopOn (X) \land A \in X) \to A \in (J fLim nei (J) (\{A\}))$
8	1	oveq2i	$⊢ J fLim L = J fLim nei (J) (\{A\})$
9	7 8	eleqtrrdi	$⊢ (J \in TopOn (X) \land A \in X) \to A \in (J fLim L)$
10	5 6 9	syl2anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F \in (J CnP K) (A)) \to A \in (J fLim L)$
11		simpr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F \in (J CnP K) (A)) \to F \in (J CnP K) (A)$
12		cnpflfi	$⊢ (A \in (J fLim L) \land F \in (J CnP K) (A)) \to F (A) \in (K fLimf L) (F)$
13	10 11 12	syl2anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F \in (J CnP K) (A)) \to F (A) \in (K fLimf L) (F)$
14	4 13	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 F (A) \in (K fLimf L) (F))$
15		simpl1	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to J \in TopOn (X)$
16		topontop	$⊢ J \in TopOn (X) \to J \in Top$
17	15 16	syl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to J \in Top$
18		simpl3	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to A \in X$
19		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
20	15 19	syl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to X = ⋃ J$
21	18 20	eleqtrd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to A \in ⋃ J$
22	1	eleq2i	$⊢ z \in L \leftrightarrow z \in nei (J) (\{A\})$
23		eqid	$⊢ ⋃ J = ⋃ J$
24	23	isneip	$⊢ (J \in Top \land A \in ⋃ J) \to (z \in nei (J) (\{A\}) \leftrightarrow (z \subseteq ⋃ J \land \exists v \in J (A \in v \land v \subseteq z)))$
25	22 24	bitrid	$⊢ (J \in Top \land A \in ⋃ J) \to (z \in L \leftrightarrow (z \subseteq ⋃ J \land \exists v \in J (A \in v \land v \subseteq z)))$
26	17 21 25	syl2anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to (z \in L \leftrightarrow (z \subseteq ⋃ J \land \exists v \in J (A \in v \land v \subseteq z)))$
27		sstr2	$⊢ F [v] \subseteq F [z] \to (F [z] \subseteq u \to F [v] \subseteq u)$
28		imass2	$⊢ v \subseteq z \to F [v] \subseteq F [z]$
29	27 28	syl11	$⊢ F [z] \subseteq u \to (v \subseteq z \to F [v] \subseteq u)$
30	29	anim2d	$⊢ F [z] \subseteq u \to ((A \in v \land v \subseteq z) \to (A \in v \land F [v] \subseteq u))$
31	30	reximdv	$⊢ F [z] \subseteq u \to (\exists v \in J (A \in v \land v \subseteq z) \to \exists v \in J (A \in v \land F [v] \subseteq u))$
32	31	com12	$⊢ \exists v \in J (A \in v \land v \subseteq z) \to (F [z] \subseteq u \to \exists v \in J (A \in v \land F [v] \subseteq u))$
33	32	adantl	$⊢ (z \subseteq ⋃ J \land \exists v \in J (A \in v \land v \subseteq z)) \to (F [z] \subseteq u \to \exists v \in J (A \in v \land F [v] \subseteq u))$
34	26 33	biimtrdi	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to (z \in L \to (F [z] \subseteq u \to \exists v \in J (A \in v \land F [v] \subseteq u)))$
35	34	rexlimdv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to (\exists z \in L F [z] \subseteq u \to \exists v \in J (A \in v \land F [v] \subseteq u))$
36	35	imim2d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to ((F (A) \in u \to \exists z \in L F [z] \subseteq u) \to (F (A) \in u \to \exists v \in J (A \in v \land F [v] \subseteq u)))$
37	36	ralimdv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to (\forall u \in K (F (A) \in u \to \exists z \in L F [z] \subseteq u) \to \forall u \in K (F (A) \in u \to \exists v \in J (A \in v \land F [v] \subseteq u)))$
38		simpr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to F : X ⟶ Y$
39	37 38	jctild	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to (\forall u \in K (F (A) \in u \to \exists z \in L F [z] \subseteq u) \to (F : X ⟶ Y \land \forall u \in K (F (A) \in u \to \exists v \in J (A \in v \land F [v] \subseteq u))))$
40	39	adantld	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to ((F (A) \in Y \land \forall u \in K (F (A) \in u \to \exists z \in L F [z] \subseteq u)) \to (F : X ⟶ Y \land \forall u \in K (F (A) \in u \to \exists v \in J (A \in v \land F [v] \subseteq u))))$
41		simpl2	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to K \in TopOn (Y)$
42	18	snssd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to \{A\} \subseteq X$
43	18	snn0d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to \{A\} \neq \emptyset$
44		neifil	$⊢ (J \in TopOn (X) \land \{A\} \subseteq X \land \{A\} \neq \emptyset) \to nei (J) (\{A\}) \in Fil (X)$
45	15 42 43 44	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)$
46	1 45	eqeltrid	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to L \in Fil (X)$
47		isflf	$⊢ (K \in TopOn (Y) \land L \in Fil (X) \land F : X ⟶ Y) \to (F (A) \in (K fLimf L) (F) \leftrightarrow (F (A) \in Y \land \forall u \in K (F (A) \in u \to \exists z \in L F [z] \subseteq u)))$
48	41 46 38 47	syl3anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to (F (A) \in (K fLimf L) (F) \leftrightarrow (F (A) \in Y \land \forall u \in K (F (A) \in u \to \exists z \in L F [z] \subseteq u)))$
49		iscnp	$⊢ (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 u \in K (F (A) \in u \to \exists v \in J (A \in v \land F [v] \subseteq u))))$
50	49	adantr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to (F \in (J CnP K) (A) \leftrightarrow (F : X ⟶ Y \land \forall u \in K (F (A) \in u \to \exists v \in J (A \in v \land F [v] \subseteq u))))$
51	40 48 50	3imtr4d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land F : X ⟶ Y) \to (F (A) \in (K fLimf L) (F) \to F \in (J CnP K) (A))$
52	51	impr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (F : X ⟶ Y \land F (A) \in (K fLimf L) (F))) \to F \in (J CnP K) (A)$
53	14 52	impbida	$⊢ (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 L) (F)))$

Metamath Proof Explorer

Theorem cnpflf2

Proof