limcfval

Description: Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	limcval.j	$⊢ J = K ↾_{𝑡} (A \cup \{B\})$
	limcval.k	$⊢ K = TopOpen (ℂ_{fld})$
Assertion	limcfval	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to (F {lim}_{ℂ} B = \{y \| (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B)\} \land F {lim}_{ℂ} B \subseteq ℂ)$

Proof

Step	Hyp	Ref	Expression
1		limcval.j	$⊢ J = K ↾_{𝑡} (A \cup \{B\})$
2		limcval.k	$⊢ K = TopOpen (ℂ_{fld})$
3		df-limc	$⊢ {lim}_{ℂ} = (f \in (ℂ ↑_{𝑝𝑚} ℂ), x \in ℂ ⟼ \{y \| \underset{˙}{[} TopOpen (ℂ_{fld}) / j \underset{˙}{]} (z \in (dom f \cup \{x\}) ⟼ if (z = x, y, f (z))) \in ((j ↾_{𝑡} (dom f \cup \{x\})) CnP j) (x)\})$
4	3	a1i	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to {lim}_{ℂ} = (f \in (ℂ ↑_{𝑝𝑚} ℂ), x \in ℂ ⟼ \{y \| \underset{˙}{[} TopOpen (ℂ_{fld}) / j \underset{˙}{]} (z \in (dom f \cup \{x\}) ⟼ if (z = x, y, f (z))) \in ((j ↾_{𝑡} (dom f \cup \{x\})) CnP j) (x)\})$
5		fvexd	$⊢ ((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \to TopOpen (ℂ_{fld}) \in V$
6		simplrl	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to f = F$
7	6	dmeqd	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to dom f = dom F$
8		simpll1	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to F : A ⟶ ℂ$
9	8	fdmd	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to dom F = A$
10	7 9	eqtrd	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to dom f = A$
11		simplrr	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to x = B$
12	11	sneqd	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to \{x\} = \{B\}$
13	10 12	uneq12d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to dom f \cup \{x\} = A \cup \{B\}$
14	11	eqeq2d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to (z = x \leftrightarrow z = B)$
15	6	fveq1d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to f (z) = F (z)$
16	14 15	ifbieq2d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to if (z = x, y, f (z)) = if (z = B, y, F (z))$
17	13 16	mpteq12dv	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to (z \in (dom f \cup \{x\}) ⟼ if (z = x, y, f (z))) = (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z)))$
18		simpr	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to j = TopOpen (ℂ_{fld})$
19	18 2	eqtr4di	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to j = K$
20	19 13	oveq12d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to j ↾_{𝑡} (dom f \cup \{x\}) = K ↾_{𝑡} (A \cup \{B\})$
21	20 1	eqtr4di	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to j ↾_{𝑡} (dom f \cup \{x\}) = J$
22	21 19	oveq12d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to (j ↾_{𝑡} (dom f \cup \{x\})) CnP j = J CnP K$
23	22 11	fveq12d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to ((j ↾_{𝑡} (dom f \cup \{x\})) CnP j) (x) = (J CnP K) (B)$
24	17 23	eleq12d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \land j = TopOpen (ℂ_{fld})) \to ((z \in (dom f \cup \{x\}) ⟼ if (z = x, y, f (z))) \in ((j ↾_{𝑡} (dom f \cup \{x\})) CnP j) (x) \leftrightarrow (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B))$
25	5 24	sbcied	$⊢ ((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \to (\underset{˙}{[} TopOpen (ℂ_{fld}) / j \underset{˙}{]} (z \in (dom f \cup \{x\}) ⟼ if (z = x, y, f (z))) \in ((j ↾_{𝑡} (dom f \cup \{x\})) CnP j) (x) \leftrightarrow (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B))$
26	25	abbidv	$⊢ ((F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \land (f = F \land x = B)) \to \{y \| \underset{˙}{[} TopOpen (ℂ_{fld}) / j \underset{˙}{]} (z \in (dom f \cup \{x\}) ⟼ if (z = x, y, f (z))) \in ((j ↾_{𝑡} (dom f \cup \{x\})) CnP j) (x)\} = \{y \| (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B)\}$
27		cnex	$⊢ ℂ \in V$
28		elpm2r	$⊢ ((ℂ \in V \land ℂ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℂ)) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
29	27 27 28	mpanl12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
30	29	3adant3	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
31		simp3	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to B \in ℂ$
32		eqid	$⊢ (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) = (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z)))$
33	1 2 32	limcvallem	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to ((z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B) \to y \in ℂ)$
34	33	abssdv	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to \{y \| (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B)\} \subseteq ℂ$
35	27	ssex	$⊢ \{y \| (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B)\} \subseteq ℂ \to \{y \| (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B)\} \in V$
36	34 35	syl	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to \{y \| (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B)\} \in V$
37	4 26 30 31 36	ovmpod	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to F {lim}_{ℂ} B = \{y \| (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B)\}$
38	37 34	eqsstrd	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to F {lim}_{ℂ} B \subseteq ℂ$
39	37 38	jca	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ \land B \in ℂ) \to (F {lim}_{ℂ} B = \{y \| (z \in (A \cup \{B\}) ⟼ if (z = B, y, F (z))) \in (J CnP K) (B)\} \land F {lim}_{ℂ} B \subseteq ℂ)$

Metamath Proof Explorer

Theorem limcfval

Proof