limcresioolb

Description: The right limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	limcresioolb.f	$⊢ φ \to F : A ⟶ ℂ$
	limcresioolb.b	$⊢ φ \to B \in ℝ$
	limcresioolb.c	$⊢ φ \to C \in ℝ^{*}$
	limcresioolb.bltc	$⊢ φ \to B < C$
	limcresioolb.bcss	$⊢ φ \to (B, C) \subseteq A$
	limcresioolb.d	$⊢ φ \to D \in ℝ^{*}$
	limcresioolb.cled	$⊢ φ \to C \leq D$
Assertion	limcresioolb	$⊢ φ \to ({F ↾}_{(B, C)}) {lim}_{ℂ} B = ({F ↾}_{(B, D)}) {lim}_{ℂ} B$

Proof

Step	Hyp	Ref	Expression
1		limcresioolb.f	$⊢ φ \to F : A ⟶ ℂ$
2		limcresioolb.b	$⊢ φ \to B \in ℝ$
3		limcresioolb.c	$⊢ φ \to C \in ℝ^{*}$
4		limcresioolb.bltc	$⊢ φ \to B < C$
5		limcresioolb.bcss	$⊢ φ \to (B, C) \subseteq A$
6		limcresioolb.d	$⊢ φ \to D \in ℝ^{*}$
7		limcresioolb.cled	$⊢ φ \to C \leq D$
8		iooss2	$⊢ (D \in ℝ^{*} \land C \leq D) \to (B, C) \subseteq (B, D)$
9	6 7 8	syl2anc	$⊢ φ \to (B, C) \subseteq (B, D)$
10	9	resabs1d	$⊢ φ \to {({F ↾}_{(B, D)}) ↾}_{(B, C)} = {F ↾}_{(B, C)}$
11	10	eqcomd	$⊢ φ \to {F ↾}_{(B, C)} = {({F ↾}_{(B, D)}) ↾}_{(B, C)}$
12	11	oveq1d	$⊢ φ \to ({F ↾}_{(B, C)}) {lim}_{ℂ} B = ({({F ↾}_{(B, D)}) ↾}_{(B, C)}) {lim}_{ℂ} B$
13		fresin	$⊢ F : A ⟶ ℂ \to ({F ↾}_{(B, D)}) : A \cap (B, D) ⟶ ℂ$
14	1 13	syl	$⊢ φ \to ({F ↾}_{(B, D)}) : A \cap (B, D) ⟶ ℂ$
15	5 9	ssind	$⊢ φ \to (B, C) \subseteq A \cap (B, D)$
16		inss2	$⊢ A \cap (B, D) \subseteq (B, D)$
17		ioosscn	$⊢ (B, D) \subseteq ℂ$
18	16 17	sstri	$⊢ A \cap (B, D) \subseteq ℂ$
19	18	a1i	$⊢ φ \to A \cap (B, D) \subseteq ℂ$
20		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
21		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})$
22	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
23		lbico1	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B < C) \to B \in [B, C)$
24	22 3 4 23	syl3anc	$⊢ φ \to B \in [B, C)$
25		snunioo1	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B < C) \to (B, C) \cup \{B\} = [B, C)$
26	22 3 4 25	syl3anc	$⊢ φ \to (B, C) \cup \{B\} = [B, C)$
27	26	fveq2d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})) ((B, C) \cup \{B\}) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})) ([B, C))$
28	20	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
29		ovex	$⊢ (B, D) \in V$
30	29	inex2	$⊢ A \cap (B, D) \in V$
31		snex	$⊢ \{B\} \in V$
32	30 31	unex	$⊢ (A \cap (B, D)) \cup \{B\} \in V$
33		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (A \cap (B, D)) \cup \{B\} \in V) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}) \in Top$
34	28 32 33	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}) \in Top$
35	34	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}) \in Top$
36		mnfxr	$⊢ −∞ \in ℝ^{*}$
37	36	a1i	$⊢ (φ \land x \in [B, C)) \to −∞ \in ℝ^{*}$
38	3	adantr	$⊢ (φ \land x \in [B, C)) \to C \in ℝ^{*}$
39		icossre	$⊢ (B \in ℝ \land C \in ℝ^{*}) \to [B, C) \subseteq ℝ$
40	2 3 39	syl2anc	$⊢ φ \to [B, C) \subseteq ℝ$
41	40	sselda	$⊢ (φ \land x \in [B, C)) \to x \in ℝ$
42	41	mnfltd	$⊢ (φ \land x \in [B, C)) \to −∞ < x$
43	22	adantr	$⊢ (φ \land x \in [B, C)) \to B \in ℝ^{*}$
44		simpr	$⊢ (φ \land x \in [B, C)) \to x \in [B, C)$
45		icoltub	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land x \in [B, C)) \to x < C$
46	43 38 44 45	syl3anc	$⊢ (φ \land x \in [B, C)) \to x < C$
47	37 38 41 42 46	eliood	$⊢ (φ \land x \in [B, C)) \to x \in (−∞, C)$
48		simpr	$⊢ (φ \land x = B) \to x = B$
49		snidg	$⊢ B \in ℝ \to B \in \{B\}$
50		elun2	$⊢ B \in \{B\} \to B \in ((A \cap (B, D)) \cup \{B\})$
51	2 49 50	3syl	$⊢ φ \to B \in ((A \cap (B, D)) \cup \{B\})$
52	51	adantr	$⊢ (φ \land x = B) \to B \in ((A \cap (B, D)) \cup \{B\})$
53	48 52	eqeltrd	$⊢ (φ \land x = B) \to x \in ((A \cap (B, D)) \cup \{B\})$
54	53	adantlr	$⊢ ((φ \land x \in [B, C)) \land x = B) \to x \in ((A \cap (B, D)) \cup \{B\})$
55		simpll	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to φ$
56	43	adantr	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to B \in ℝ^{*}$
57	38	adantr	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to C \in ℝ^{*}$
58	41	adantr	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to x \in ℝ$
59	2	ad2antrr	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to B \in ℝ$
60		icogelb	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land x \in [B, C)) \to B \leq x$
61	43 38 44 60	syl3anc	$⊢ (φ \land x \in [B, C)) \to B \leq x$
62	61	adantr	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to B \leq x$
63		neqne	$⊢ \neg x = B \to x \neq B$
64	63	adantl	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to x \neq B$
65	59 58 62 64	leneltd	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to B < x$
66	46	adantr	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to x < C$
67	56 57 58 65 66	eliood	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to x \in (B, C)$
68	15	sselda	$⊢ (φ \land x \in (B, C)) \to x \in (A \cap (B, D))$
69		elun1	$⊢ x \in (A \cap (B, D)) \to x \in ((A \cap (B, D)) \cup \{B\})$
70	68 69	syl	$⊢ (φ \land x \in (B, C)) \to x \in ((A \cap (B, D)) \cup \{B\})$
71	55 67 70	syl2anc	$⊢ ((φ \land x \in [B, C)) \land \neg x = B) \to x \in ((A \cap (B, D)) \cup \{B\})$
72	54 71	pm2.61dan	$⊢ (φ \land x \in [B, C)) \to x \in ((A \cap (B, D)) \cup \{B\})$
73	47 72	elind	$⊢ (φ \land x \in [B, C)) \to x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))$
74	24	adantr	$⊢ (φ \land x = B) \to B \in [B, C)$
75	48 74	eqeltrd	$⊢ (φ \land x = B) \to x \in [B, C)$
76	75	adantlr	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land x = B) \to x \in [B, C)$
77		ioossico	$⊢ (B, C) \subseteq [B, C)$
78	22	ad2antrr	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land \neg x = B) \to B \in ℝ^{*}$
79	3	ad2antrr	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land \neg x = B) \to C \in ℝ^{*}$
80		elinel1	$⊢ x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\})) \to x \in (−∞, C)$
81	80	elioored	$⊢ x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\})) \to x \in ℝ$
82	81	ad2antlr	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land \neg x = B) \to x \in ℝ$
83	6	ad2antrr	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land \neg x = B) \to D \in ℝ^{*}$
84		elinel2	$⊢ x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\})) \to x \in ((A \cap (B, D)) \cup \{B\})$
85		id	$⊢ \neg x = B \to \neg x = B$
86		velsn	$⊢ x \in \{B\} \leftrightarrow x = B$
87	85 86	sylnibr	$⊢ \neg x = B \to \neg x \in \{B\}$
88		elunnel2	$⊢ (x \in ((A \cap (B, D)) \cup \{B\}) \land \neg x \in \{B\}) \to x \in (A \cap (B, D))$
89	84 87 88	syl2an	$⊢ (x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\})) \land \neg x = B) \to x \in (A \cap (B, D))$
90	16 89	sselid	$⊢ (x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\})) \land \neg x = B) \to x \in (B, D)$
91	90	adantll	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land \neg x = B) \to x \in (B, D)$
92		ioogtlb	$⊢ (B \in ℝ^{} \land D \in ℝ^{} \land x \in (B, D)) \to B < x$
93	78 83 91 92	syl3anc	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land \neg x = B) \to B < x$
94	36	a1i	$⊢ (φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \to −∞ \in ℝ^{*}$
95	3	adantr	$⊢ (φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \to C \in ℝ^{*}$
96	80	adantl	$⊢ (φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \to x \in (−∞, C)$
97		iooltub	$⊢ (−∞ \in ℝ^{} \land C \in ℝ^{} \land x \in (−∞, C)) \to x < C$
98	94 95 96 97	syl3anc	$⊢ (φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \to x < C$
99	98	adantr	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land \neg x = B) \to x < C$
100	78 79 82 93 99	eliood	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land \neg x = B) \to x \in (B, C)$
101	77 100	sselid	$⊢ ((φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \land \neg x = B) \to x \in [B, C)$
102	76 101	pm2.61dan	$⊢ (φ \land x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\}))) \to x \in [B, C)$
103	73 102	impbida	$⊢ φ \to (x \in [B, C) \leftrightarrow x \in ((−∞, C) \cap ((A \cap (B, D)) \cup \{B\})))$
104	103	eqrdv	$⊢ φ \to [B, C) = (−∞, C) \cap ((A \cap (B, D)) \cup \{B\})$
105		retop	$⊢ topGen (ran (.)) \in Top$
106	105	a1i	$⊢ φ \to topGen (ran (.)) \in Top$
107	32	a1i	$⊢ φ \to (A \cap (B, D)) \cup \{B\} \in V$
108		iooretop	$⊢ (−∞, C) \in topGen (ran (.))$
109	108	a1i	$⊢ φ \to (−∞, C) \in topGen (ran (.))$
110		elrestr	$⊢ (topGen (ran (.)) \in Top \land (A \cap (B, D)) \cup \{B\} \in V \land (−∞, C) \in topGen (ran (.))) \to (−∞, C) \cap ((A \cap (B, D)) \cup \{B\}) \in (topGen (ran (.)) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}))$
111	106 107 109 110	syl3anc	$⊢ φ \to (−∞, C) \cap ((A \cap (B, D)) \cup \{B\}) \in (topGen (ran (.)) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}))$
112	104 111	eqeltrd	$⊢ φ \to [B, C) \in (topGen (ran (.)) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}))$
113		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
114	113	oveq1i	$⊢ topGen (ran (.)) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}) = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})$
115	28	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
116		ioossre	$⊢ (B, D) \subseteq ℝ$
117	16 116	sstri	$⊢ A \cap (B, D) \subseteq ℝ$
118	117	a1i	$⊢ φ \to A \cap (B, D) \subseteq ℝ$
119	2	snssd	$⊢ φ \to \{B\} \subseteq ℝ$
120	118 119	unssd	$⊢ φ \to (A \cap (B, D)) \cup \{B\} \subseteq ℝ$
121		reex	$⊢ ℝ \in V$
122	121	a1i	$⊢ φ \to ℝ \in V$
123		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (A \cap (B, D)) \cup \{B\} \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})$
124	115 120 122 123	syl3anc	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})$
125	114 124	eqtrid	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})$
126	112 125	eleqtrd	$⊢ φ \to [B, C) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}))$
127		isopn3i	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}) \in Top \land [B, C) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\}))) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})) ([B, C)) = [B, C)$
128	35 126 127	syl2anc	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})) ([B, C)) = [B, C)$
129	27 128	eqtr2d	$⊢ φ \to [B, C) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})) ((B, C) \cup \{B\})$
130	24 129	eleqtrd	$⊢ φ \to B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (B, D)) \cup \{B\})) ((B, C) \cup \{B\})$
131	14 15 19 20 21 130	limcres	$⊢ φ \to ({({F ↾}_{(B, D)}) ↾}_{(B, C)}) {lim}_{ℂ} B = ({F ↾}_{(B, D)}) {lim}_{ℂ} B$
132	12 131	eqtrd	$⊢ φ \to ({F ↾}_{(B, C)}) {lim}_{ℂ} B = ({F ↾}_{(B, D)}) {lim}_{ℂ} B$

Metamath Proof Explorer

Theorem limcresioolb

Proof