cnplimc

Description: A function is continuous at B iff its limit at B equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	cnplimc.k	$⊢ K = TopOpen (ℂ_{fld})$
	cnplimc.j	$⊢ J = K ↾_{𝑡} A$
Assertion	cnplimc	$⊢ (A \subseteq ℂ \land B \in A) \to (F \in (J CnP K) (B) \leftrightarrow (F : A ⟶ ℂ \land F (B) \in (F {lim}_{ℂ} B)))$

Proof

Step	Hyp	Ref	Expression
1		cnplimc.k	$⊢ K = TopOpen (ℂ_{fld})$
2		cnplimc.j	$⊢ J = K ↾_{𝑡} A$
3	1	cnfldtopon	$⊢ K \in TopOn (ℂ)$
4		simpl	$⊢ (A \subseteq ℂ \land B \in A) \to A \subseteq ℂ$
5		resttopon	$⊢ (K \in TopOn (ℂ) \land A \subseteq ℂ) \to K ↾_{𝑡} A \in TopOn (A)$
6	3 4 5	sylancr	$⊢ (A \subseteq ℂ \land B \in A) \to K ↾_{𝑡} A \in TopOn (A)$
7	2 6	eqeltrid	$⊢ (A \subseteq ℂ \land B \in A) \to J \in TopOn (A)$
8		cnpf2	$⊢ (J \in TopOn (A) \land K \in TopOn (ℂ) \land F \in (J CnP K) (B)) \to F : A ⟶ ℂ$
9	8	3expia	$⊢ (J \in TopOn (A) \land K \in TopOn (ℂ)) \to (F \in (J CnP K) (B) \to F : A ⟶ ℂ)$
10	7 3 9	sylancl	$⊢ (A \subseteq ℂ \land B \in A) \to (F \in (J CnP K) (B) \to F : A ⟶ ℂ)$
11	10	pm4.71rd	$⊢ (A \subseteq ℂ \land B \in A) \to (F \in (J CnP K) (B) \leftrightarrow (F : A ⟶ ℂ \land F \in (J CnP K) (B)))$
12		simpr	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to F : A ⟶ ℂ$
13		simplr	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to B \in A$
14	13	snssd	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to \{B\} \subseteq A$
15		ssequn2	$⊢ \{B\} \subseteq A \leftrightarrow A \cup \{B\} = A$
16	14 15	sylib	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to A \cup \{B\} = A$
17	16	feq2d	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to (F : A \cup \{B\} ⟶ ℂ \leftrightarrow F : A ⟶ ℂ)$
18	12 17	mpbird	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to F : A \cup \{B\} ⟶ ℂ$
19	18	feqmptd	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to F = (x \in (A \cup \{B\}) ⟼ F (x))$
20	16	oveq2d	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to K ↾_{𝑡} (A \cup \{B\}) = K ↾_{𝑡} A$
21	2 20	eqtr4id	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to J = K ↾_{𝑡} (A \cup \{B\})$
22	21	oveq1d	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to J CnP K = (K ↾_{𝑡} (A \cup \{B\})) CnP K$
23	22	fveq1d	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to (J CnP K) (B) = ((K ↾_{𝑡} (A \cup \{B\})) CnP K) (B)$
24	19 23	eleq12d	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to (F \in (J CnP K) (B) \leftrightarrow (x \in (A \cup \{B\}) ⟼ F (x)) \in ((K ↾_{𝑡} (A \cup \{B\})) CnP K) (B))$
25		eqid	$⊢ K ↾_{𝑡} (A \cup \{B\}) = K ↾_{𝑡} (A \cup \{B\})$
26		ifid	$⊢ if (x = B, F (x), F (x)) = F (x)$
27		fveq2	$⊢ x = B \to F (x) = F (B)$
28	27	adantl	$⊢ (x \in (A \cup \{B\}) \land x = B) \to F (x) = F (B)$
29	28	ifeq1da	$⊢ x \in (A \cup \{B\}) \to if (x = B, F (x), F (x)) = if (x = B, F (B), F (x))$
30	26 29	eqtr3id	$⊢ x \in (A \cup \{B\}) \to F (x) = if (x = B, F (B), F (x))$
31	30	mpteq2ia	$⊢ (x \in (A \cup \{B\}) ⟼ F (x)) = (x \in (A \cup \{B\}) ⟼ if (x = B, F (B), F (x)))$
32		simpll	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to A \subseteq ℂ$
33	32 13	sseldd	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to B \in ℂ$
34	25 1 31 12 32 33	ellimc	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to (F (B) \in (F {lim}_{ℂ} B) \leftrightarrow (x \in (A \cup \{B\}) ⟼ F (x)) \in ((K ↾_{𝑡} (A \cup \{B\})) CnP K) (B))$
35	24 34	bitr4d	$⊢ ((A \subseteq ℂ \land B \in A) \land F : A ⟶ ℂ) \to (F \in (J CnP K) (B) \leftrightarrow F (B) \in (F {lim}_{ℂ} B))$
36	35	pm5.32da	$⊢ (A \subseteq ℂ \land B \in A) \to ((F : A ⟶ ℂ \land F \in (J CnP K) (B)) \leftrightarrow (F : A ⟶ ℂ \land F (B) \in (F {lim}_{ℂ} B)))$
37	11 36	bitrd	$⊢ (A \subseteq ℂ \land B \in A) \to (F \in (J CnP K) (B) \leftrightarrow (F : A ⟶ ℂ \land F (B) \in (F {lim}_{ℂ} B)))$

Metamath Proof Explorer

Theorem cnplimc

Proof