icocncflimc

Description: Limit at the lower bound, of a continuous function defined on a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	icocncflimc.a	$⊢ φ \to A \in ℝ$
	icocncflimc.b	$⊢ φ \to B \in ℝ^{*}$
	icocncflimc.altb	$⊢ φ \to A < B$
	icocncflimc.f	$⊢ φ \to F : [A, B) \underset{cn}{⟶} ℂ$
Assertion	icocncflimc	$⊢ φ \to F (A) \in (({F ↾}_{(A, B)}) {lim}_{ℂ} A)$

Proof

Step	Hyp	Ref	Expression
1		icocncflimc.a	$⊢ φ \to A \in ℝ$
2		icocncflimc.b	$⊢ φ \to B \in ℝ^{*}$
3		icocncflimc.altb	$⊢ φ \to A < B$
4		icocncflimc.f	$⊢ φ \to F : [A, B) \underset{cn}{⟶} ℂ$
5	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
6	1	leidd	$⊢ φ \to A \leq A$
7	5 2 5 6 3	elicod	$⊢ φ \to A \in [A, B)$
8	4 7	cnlimci	$⊢ φ \to F (A) \in (F {lim}_{ℂ} A)$
9		cncfrss	$⊢ F : [A, B) \underset{cn}{⟶} ℂ \to [A, B) \subseteq ℂ$
10	4 9	syl	$⊢ φ \to [A, B) \subseteq ℂ$
11		ssid	$⊢ ℂ \subseteq ℂ$
12		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
13		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)$
14		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
15	12 13 14	cncfcn	$⊢ ([A, B) \subseteq ℂ \land ℂ \subseteq ℂ) \to [A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
16	10 11 15	sylancl	$⊢ φ \to [A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
17	4 16	eleqtrd	$⊢ φ \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ))$
18	12	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
19	18	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
20		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land [A, B) \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B) \in TopOn ([A, B))$
21	19 10 20	syl2anc	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B) \in TopOn ([A, B))$
22	12	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
23		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
24	23	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
25	22 24	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
26	25	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ \in TopOn (ℂ)$
27		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B) \in TopOn ([A, B)) \land TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ \in TopOn (ℂ)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) \leftrightarrow (F : [A, B) ⟶ ℂ \land \forall x \in [A, B) F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) (x)))$
28	21 26 27	sylancl	$⊢ φ \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) \leftrightarrow (F : [A, B) ⟶ ℂ \land \forall x \in [A, B) F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) (x)))$
29	17 28	mpbid	$⊢ φ \to (F : [A, B) ⟶ ℂ \land \forall x \in [A, B) F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) (x))$
30	29	simpld	$⊢ φ \to F : [A, B) ⟶ ℂ$
31		ioossico	$⊢ (A, B) \subseteq [A, B)$
32	31	a1i	$⊢ φ \to (A, B) \subseteq [A, B)$
33		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B) \cup \{A\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B) \cup \{A\})$
34	1	recnd	$⊢ φ \to A \in ℂ$
35	23	ntrtop	$⊢ TopOpen (ℂ_{fld}) \in Top \to int (TopOpen (ℂ_{fld})) (ℂ) = ℂ$
36	22 35	ax-mp	$⊢ int (TopOpen (ℂ_{fld})) (ℂ) = ℂ$
37		undif	$⊢ [A, B) \subseteq ℂ \leftrightarrow [A, B) \cup (ℂ ∖ [A, B)) = ℂ$
38	10 37	sylib	$⊢ φ \to [A, B) \cup (ℂ ∖ [A, B)) = ℂ$
39	38	eqcomd	$⊢ φ \to ℂ = [A, B) \cup (ℂ ∖ [A, B))$
40	39	fveq2d	$⊢ φ \to int (TopOpen (ℂ_{fld})) (ℂ) = int (TopOpen (ℂ_{fld})) ([A, B) \cup (ℂ ∖ [A, B)))$
41	36 40	eqtr3id	$⊢ φ \to ℂ = int (TopOpen (ℂ_{fld})) ([A, B) \cup (ℂ ∖ [A, B)))$
42	34 41	eleqtrd	$⊢ φ \to A \in int (TopOpen (ℂ_{fld})) ([A, B) \cup (ℂ ∖ [A, B)))$
43	42 7	elind	$⊢ φ \to A \in (int (TopOpen (ℂ_{fld})) ([A, B) \cup (ℂ ∖ [A, B))) \cap [A, B))$
44	22	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
45		ssid	$⊢ [A, B) \subseteq [A, B)$
46	45	a1i	$⊢ φ \to [A, B) \subseteq [A, B)$
47	23 13	restntr	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [A, B) \subseteq ℂ \land [A, B) \subseteq [A, B)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) ([A, B)) = int (TopOpen (ℂ_{fld})) ([A, B) \cup (ℂ ∖ [A, B))) \cap [A, B)$
48	44 10 46 47	syl3anc	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) ([A, B)) = int (TopOpen (ℂ_{fld})) ([A, B) \cup (ℂ ∖ [A, B))) \cap [A, B)$
49	43 48	eleqtrrd	$⊢ φ \to A \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) ([A, B))$
50	7	snssd	$⊢ φ \to \{A\} \subseteq [A, B)$
51		ssequn2	$⊢ \{A\} \subseteq [A, B) \leftrightarrow [A, B) \cup \{A\} = [A, B)$
52	50 51	sylib	$⊢ φ \to [A, B) \cup \{A\} = [A, B)$
53	52	eqcomd	$⊢ φ \to [A, B) = [A, B) \cup \{A\}$
54	53	oveq2d	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B) \cup \{A\})$
55	54	fveq2d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B) \cup \{A\}))$
56		snunioo1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (A, B) \cup \{A\} = [A, B)$
57	5 2 3 56	syl3anc	$⊢ φ \to (A, B) \cup \{A\} = [A, B)$
58	57	eqcomd	$⊢ φ \to [A, B) = (A, B) \cup \{A\}$
59	55 58	fveq12d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)) ([A, B)) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B) \cup \{A\})) ((A, B) \cup \{A\})$
60	49 59	eleqtrd	$⊢ φ \to A \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B) \cup \{A\})) ((A, B) \cup \{A\})$
61	30 32 10 12 33 60	limcres	$⊢ φ \to ({F ↾}_{(A, B)}) {lim}_{ℂ} A = F {lim}_{ℂ} A$
62	8 61	eleqtrrd	$⊢ φ \to F (A) \in (({F ↾}_{(A, B)}) {lim}_{ℂ} A)$

Metamath Proof Explorer

Theorem icocncflimc

Proof