limcdif

Description: It suffices to consider functions which are not defined at B to define the limit of a function. In particular, the value of the original function F at B does not affect the limit of F . (Contributed by Mario Carneiro, 25-Dec-2016)

		Ref	Expression
	Hypothesis	limccl.f	$⊢ φ \to F : A ⟶ ℂ$
	Assertion	limcdif	$⊢ φ \to F {lim}_{ℂ} B = ({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B$

Proof

Step	Hyp	Ref	Expression
1		limccl.f	$⊢ φ \to F : A ⟶ ℂ$
2	1	fdmd	$⊢ φ \to dom F = A$
3	2	adantr	$⊢ (φ \land x \in (F {lim}_{ℂ} B)) \to dom F = A$
4		limcrcl	$⊢ x \in (F {lim}_{ℂ} B) \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land B \in ℂ)$
5	4	adantl	$⊢ (φ \land x \in (F {lim}_{ℂ} B)) \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land B \in ℂ)$
6	5	simp2d	$⊢ (φ \land x \in (F {lim}_{ℂ} B)) \to dom F \subseteq ℂ$
7	3 6	eqsstrrd	$⊢ (φ \land x \in (F {lim}_{ℂ} B)) \to A \subseteq ℂ$
8	5	simp3d	$⊢ (φ \land x \in (F {lim}_{ℂ} B)) \to B \in ℂ$
9	7 8	jca	$⊢ (φ \land x \in (F {lim}_{ℂ} B)) \to (A \subseteq ℂ \land B \in ℂ)$
10	9	ex	$⊢ φ \to (x \in (F {lim}_{ℂ} B) \to (A \subseteq ℂ \land B \in ℂ))$
11		undif1	$⊢ (A ∖ \{B\}) \cup \{B\} = A \cup \{B\}$
12		difss	$⊢ A ∖ \{B\} \subseteq A$
13		fssres	$⊢ (F : A ⟶ ℂ \land A ∖ \{B\} \subseteq A) \to ({F ↾}_{(A ∖ \{B\})}) : A ∖ \{B\} ⟶ ℂ$
14	1 12 13	sylancl	$⊢ φ \to ({F ↾}_{(A ∖ \{B\})}) : A ∖ \{B\} ⟶ ℂ$
15	14	fdmd	$⊢ φ \to dom ({F ↾}_{(A ∖ \{B\})}) = A ∖ \{B\}$
16	15	adantr	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to dom ({F ↾}_{(A ∖ \{B\})}) = A ∖ \{B\}$
17		limcrcl	$⊢ x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B) \to (({F ↾}_{(A ∖ \{B\})}) : dom ({F ↾}_{(A ∖ \{B\})}) ⟶ ℂ \land dom ({F ↾}_{(A ∖ \{B\})}) \subseteq ℂ \land B \in ℂ)$
18	17	adantl	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to (({F ↾}_{(A ∖ \{B\})}) : dom ({F ↾}_{(A ∖ \{B\})}) ⟶ ℂ \land dom ({F ↾}_{(A ∖ \{B\})}) \subseteq ℂ \land B \in ℂ)$
19	18	simp2d	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to dom ({F ↾}_{(A ∖ \{B\})}) \subseteq ℂ$
20	16 19	eqsstrrd	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to A ∖ \{B\} \subseteq ℂ$
21	18	simp3d	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to B \in ℂ$
22	21	snssd	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to \{B\} \subseteq ℂ$
23	20 22	unssd	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to (A ∖ \{B\}) \cup \{B\} \subseteq ℂ$
24	11 23	eqsstrrid	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to A \cup \{B\} \subseteq ℂ$
25	24	unssad	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to A \subseteq ℂ$
26	25 21	jca	$⊢ (φ \land x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)) \to (A \subseteq ℂ \land B \in ℂ)$
27	26	ex	$⊢ φ \to (x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B) \to (A \subseteq ℂ \land B \in ℂ))$
28		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cup \{B\})$
29		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
30		eqid	$⊢ (z \in (A \cup \{B\}) ⟼ if (z = B, x, F (z))) = (z \in (A \cup \{B\}) ⟼ if (z = B, x, F (z)))$
31	1	adantr	$⊢ (φ \land (A \subseteq ℂ \land B \in ℂ)) \to F : A ⟶ ℂ$
32		simprl	$⊢ (φ \land (A \subseteq ℂ \land B \in ℂ)) \to A \subseteq ℂ$
33		simprr	$⊢ (φ \land (A \subseteq ℂ \land B \in ℂ)) \to B \in ℂ$
34	28 29 30 31 32 33	ellimc	$⊢ (φ \land (A \subseteq ℂ \land B \in ℂ)) \to (x \in (F {lim}_{ℂ} B) \leftrightarrow (z \in (A \cup \{B\}) ⟼ if (z = B, x, F (z))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cup \{B\})) CnP TopOpen (ℂ_{fld})) (B))$
35	11	eqcomi	$⊢ A \cup \{B\} = (A ∖ \{B\}) \cup \{B\}$
36	35	oveq2i	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A ∖ \{B\}) \cup \{B\})$
37	35	mpteq1i	$⊢ (z \in (A \cup \{B\}) ⟼ if (z = B, x, F (z))) = (z \in ((A ∖ \{B\}) \cup \{B\}) ⟼ if (z = B, x, F (z)))$
38		elun	$⊢ z \in ((A ∖ \{B\}) \cup \{B\}) \leftrightarrow (z \in (A ∖ \{B\}) \lor z \in \{B\})$
39		velsn	$⊢ z \in \{B\} \leftrightarrow z = B$
40	39	orbi2i	$⊢ (z \in (A ∖ \{B\}) \lor z \in \{B\}) \leftrightarrow (z \in (A ∖ \{B\}) \lor z = B)$
41		pm5.61	$⊢ ((z \in (A ∖ \{B\}) \lor z = B) \land \neg z = B) \leftrightarrow (z \in (A ∖ \{B\}) \land \neg z = B)$
42		fvres	$⊢ z \in (A ∖ \{B\}) \to ({F ↾}_{(A ∖ \{B\})}) (z) = F (z)$
43	42	adantr	$⊢ (z \in (A ∖ \{B\}) \land \neg z = B) \to ({F ↾}_{(A ∖ \{B\})}) (z) = F (z)$
44	41 43	sylbi	$⊢ ((z \in (A ∖ \{B\}) \lor z = B) \land \neg z = B) \to ({F ↾}_{(A ∖ \{B\})}) (z) = F (z)$
45	44	ifeq2da	$⊢ (z \in (A ∖ \{B\}) \lor z = B) \to if (z = B, x, ({F ↾}_{(A ∖ \{B\})}) (z)) = if (z = B, x, F (z))$
46	40 45	sylbi	$⊢ (z \in (A ∖ \{B\}) \lor z \in \{B\}) \to if (z = B, x, ({F ↾}_{(A ∖ \{B\})}) (z)) = if (z = B, x, F (z))$
47	38 46	sylbi	$⊢ z \in ((A ∖ \{B\}) \cup \{B\}) \to if (z = B, x, ({F ↾}_{(A ∖ \{B\})}) (z)) = if (z = B, x, F (z))$
48	47	mpteq2ia	$⊢ (z \in ((A ∖ \{B\}) \cup \{B\}) ⟼ if (z = B, x, ({F ↾}_{(A ∖ \{B\})}) (z))) = (z \in ((A ∖ \{B\}) \cup \{B\}) ⟼ if (z = B, x, F (z)))$
49	37 48	eqtr4i	$⊢ (z \in (A \cup \{B\}) ⟼ if (z = B, x, F (z))) = (z \in ((A ∖ \{B\}) \cup \{B\}) ⟼ if (z = B, x, ({F ↾}_{(A ∖ \{B\})}) (z)))$
50	14	adantr	$⊢ (φ \land (A \subseteq ℂ \land B \in ℂ)) \to ({F ↾}_{(A ∖ \{B\})}) : A ∖ \{B\} ⟶ ℂ$
51	32	ssdifssd	$⊢ (φ \land (A \subseteq ℂ \land B \in ℂ)) \to A ∖ \{B\} \subseteq ℂ$
52	36 29 49 50 51 33	ellimc	$⊢ (φ \land (A \subseteq ℂ \land B \in ℂ)) \to (x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B) \leftrightarrow (z \in (A \cup \{B\}) ⟼ if (z = B, x, F (z))) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A \cup \{B\})) CnP TopOpen (ℂ_{fld})) (B))$
53	34 52	bitr4d	$⊢ (φ \land (A \subseteq ℂ \land B \in ℂ)) \to (x \in (F {lim}_{ℂ} B) \leftrightarrow x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B))$
54	53	ex	$⊢ φ \to ((A \subseteq ℂ \land B \in ℂ) \to (x \in (F {lim}_{ℂ} B) \leftrightarrow x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B)))$
55	10 27 54	pm5.21ndd	$⊢ φ \to (x \in (F {lim}_{ℂ} B) \leftrightarrow x \in (({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B))$
56	55	eqrdv	$⊢ φ \to F {lim}_{ℂ} B = ({F ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B$

Metamath Proof Explorer

Theorem limcdif

Proof