Theorem limcresioolb 38710

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

Hypotheses

Ref	Expression
limcresioolb.f	⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
limcresioolb.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
limcresioolb.c	⊢ (𝜑 → 𝐶 ∈ ℝ*)
limcresioolb.bltc	⊢ (𝜑 → 𝐵 < 𝐶)
limcresioolb.bcss	⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴)
limcresioolb.d	⊢ (𝜑 → 𝐷 ∈ ℝ*)
limcresioolb.cled	⊢ (𝜑 → 𝐶 ≤ 𝐷)

Assertion

Ref	Expression
limcresioolb	⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐵) = ((𝐹 ↾ (𝐵(,)𝐷)) limℂ 𝐵))

Proof of Theorem limcresioolb

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		limcresioolb.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ ℝ*)
2		limcresioolb.cled	. . . . . 6 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
3		iooss2 12082	. . . . . 6 ⊢ ((𝐷 ∈ ℝ* ∧ 𝐶 ≤ 𝐷) → (𝐵(,)𝐶) ⊆ (𝐵(,)𝐷))
4	1, 2, 3	syl2anc 691	. . . . 5 ⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐵(,)𝐷))
5	4	resabs1d 5348	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐷)) ↾ (𝐵(,)𝐶)) = (𝐹 ↾ (𝐵(,)𝐶)))
6	5	eqcomd 2616	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐵(,)𝐶)) = ((𝐹 ↾ (𝐵(,)𝐷)) ↾ (𝐵(,)𝐶)))
7	6	oveq1d 6564	. 2 ⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐵) = (((𝐹 ↾ (𝐵(,)𝐷)) ↾ (𝐵(,)𝐶)) limℂ 𝐵))
8		limcresioolb.f	. . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
9		fresin 5986	. . . 4 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)𝐷)):(𝐴 ∩ (𝐵(,)𝐷))⟶ℂ)
10	8, 9	syl 17	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐵(,)𝐷)):(𝐴 ∩ (𝐵(,)𝐷))⟶ℂ)
11		limcresioolb.bcss	. . . 4 ⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴)
12	11, 4	ssind 3799	. . 3 ⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐴 ∩ (𝐵(,)𝐷)))
13		inss2 3796	. . . . 5 ⊢ (𝐴 ∩ (𝐵(,)𝐷)) ⊆ (𝐵(,)𝐷)
14		ioosscn 38563	. . . . 5 ⊢ (𝐵(,)𝐷) ⊆ ℂ
15	13, 14	sstri 3577	. . . 4 ⊢ (𝐴 ∩ (𝐵(,)𝐷)) ⊆ ℂ
16	15	a1i 11	. . 3 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)𝐷)) ⊆ ℂ)
17		eqid 2610	. . 3 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
18		eqid 2610	. . 3 ⊢ ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
19		limcresioolb.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
20	19	rexrd 9968	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
21		limcresioolb.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ*)
22		limcresioolb.bltc	. . . . 5 ⊢ (𝜑 → 𝐵 < 𝐶)
23		lbico1 12099	. . . . 5 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 < 𝐶) → 𝐵 ∈ (𝐵[,)𝐶))
24	20, 21, 22, 23	syl3anc 1318	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐵[,)𝐶))
25		snunioo1 38585	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 < 𝐶) → ((𝐵(,)𝐶) ∪ {𝐵}) = (𝐵[,)𝐶))
26	20, 21, 22, 25	syl3anc 1318	. . . . . 6 ⊢ (𝜑 → ((𝐵(,)𝐶) ∪ {𝐵}) = (𝐵[,)𝐶))
27	26	fveq2d 6107	. . . . 5 ⊢ (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘((𝐵(,)𝐶) ∪ {𝐵})) = ((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘(𝐵[,)𝐶)))
28	17	cnfldtop 22397	. . . . . . . 8 ⊢ (TopOpen‘ℂfld) ∈ Top
29		ovex 6577	. . . . . . . . . 10 ⊢ (𝐵(,)𝐷) ∈ V
30	29	inex2 4728	. . . . . . . . 9 ⊢ (𝐴 ∩ (𝐵(,)𝐷)) ∈ V
31		snex 4835	. . . . . . . . 9 ⊢ {𝐵} ∈ V
32	30, 31	unex 6854	. . . . . . . 8 ⊢ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∈ V
33		resttop 20774	. . . . . . . 8 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∈ V) → ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ Top)
34	28, 32, 33	mp2an 704	. . . . . . 7 ⊢ ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ Top
35	34	a1i 11	. . . . . 6 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ Top)
36		mnfxr 9975	. . . . . . . . . . . . 13 ⊢ -∞ ∈ ℝ*
37	36	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → -∞ ∈ ℝ*)
38	21	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝐶 ∈ ℝ*)
39		icossre 12125	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ*) → (𝐵[,)𝐶) ⊆ ℝ)
40	19, 21, 39	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵[,)𝐶) ⊆ ℝ)
41	40	sselda 3568	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ ℝ)
42	41	mnfltd 11834	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → -∞ < 𝑥)
43	20	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝐵 ∈ ℝ*)
44		simpr 476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ (𝐵[,)𝐶))
45		icoltub 38579	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 < 𝐶)
46	43, 38, 44, 45	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 < 𝐶)
47	37, 38, 41, 42, 46	eliood 38567	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ (-∞(,)𝐶))
48		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵)
49		snidg 4153	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ {𝐵})
50		elun2 3743	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ {𝐵} → 𝐵 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
51	19, 49, 50	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
52	51	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐵 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
53	48, 52	eqeltrd 2688	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
54	53	adantlr 747	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
55		simpll 786	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝜑)
56	43	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ*)
57	38	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐶 ∈ ℝ*)
58	41	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ)
59	19	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ)
60		icogelb 12096	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝐵 ≤ 𝑥)
61	43, 38, 44, 60	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝐵 ≤ 𝑥)
62	61	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ≤ 𝑥)
63		neqne 2790	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 = 𝐵 → 𝑥 ≠ 𝐵)
64	63	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ≠ 𝐵)
65	59, 58, 62, 64	leneltd 10070	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 < 𝑥)
66	46	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐶)
67	56, 57, 58, 65, 66	eliood 38567	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵(,)𝐶))
68	12	sselda 3568	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐴 ∩ (𝐵(,)𝐷)))
69		elun1 3742	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴 ∩ (𝐵(,)𝐷)) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
70	68, 69	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
71	55, 67, 70	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
72	54, 71	pm2.61dan 828	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
73	47, 72	elind 3760	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))
74	24	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐵 ∈ (𝐵[,)𝐶))
75	48, 74	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵[,)𝐶))
76	75	adantlr 747	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵[,)𝐶))
77		ioossico 12133	. . . . . . . . . . . 12 ⊢ (𝐵(,)𝐶) ⊆ (𝐵[,)𝐶)
78	20	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ*)
79	21	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝐶 ∈ ℝ*)
80		elinel1 3761	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) → 𝑥 ∈ (-∞(,)𝐶))
81		elioore 12076	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-∞(,)𝐶) → 𝑥 ∈ ℝ)
82	80, 81	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) → 𝑥 ∈ ℝ)
83	82	ad2antlr 759	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ)
84	1	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝐷 ∈ ℝ*)
85		elinel2 3762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
86		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑥 = 𝐵 → ¬ 𝑥 = 𝐵)
87		velsn 4141	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
88	86, 87	sylnibr 318	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 = 𝐵 → ¬ 𝑥 ∈ {𝐵})
89		elunnel2 38221	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∧ ¬ 𝑥 ∈ {𝐵}) → 𝑥 ∈ (𝐴 ∩ (𝐵(,)𝐷)))
90	85, 88, 89	syl2an 493	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴 ∩ (𝐵(,)𝐷)))
91	13, 90	sseldi 3566	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵(,)𝐷))
92	91	adantll 746	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵(,)𝐷))
93		ioogtlb 38564	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝑥 ∈ (𝐵(,)𝐷)) → 𝐵 < 𝑥)
94	78, 84, 92, 93	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝐵 < 𝑥)
95	36	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → -∞ ∈ ℝ*)
96	21	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → 𝐶 ∈ ℝ*)
97	80	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → 𝑥 ∈ (-∞(,)𝐶))
98		iooltub 38582	. . . . . . . . . . . . . . 15 ⊢ ((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ (-∞(,)𝐶)) → 𝑥 < 𝐶)
99	95, 96, 97, 98	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → 𝑥 < 𝐶)
100	99	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐶)
101	78, 79, 83, 94, 100	eliood 38567	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵(,)𝐶))
102	77, 101	sseldi 3566	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵[,)𝐶))
103	76, 102	pm2.61dan 828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → 𝑥 ∈ (𝐵[,)𝐶))
104	73, 103	impbida 873	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐵[,)𝐶) ↔ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))))
105	104	eqrdv 2608	. . . . . . . 8 ⊢ (𝜑 → (𝐵[,)𝐶) = ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))
106		retop 22375	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) ∈ Top
107	106	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (topGen‘ran (,)) ∈ Top)
108	32	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∈ V)
109		iooretop 22379	. . . . . . . . . 10 ⊢ (-∞(,)𝐶) ∈ (topGen‘ran (,))
110	109	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (-∞(,)𝐶) ∈ (topGen‘ran (,)))
111		elrestr 15912	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∈ V ∧ (-∞(,)𝐶) ∈ (topGen‘ran (,))) → ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))
112	107, 108, 110, 111	syl3anc 1318	. . . . . . . 8 ⊢ (𝜑 → ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))
113	105, 112	eqeltrd 2688	. . . . . . 7 ⊢ (𝜑 → (𝐵[,)𝐶) ∈ ((topGen‘ran (,)) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))
114	17	tgioo2 22414	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
115	114	oveq1i 6559	. . . . . . . 8 ⊢ ((topGen‘ran (,)) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))
116	28	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (TopOpen‘ℂfld) ∈ Top)
117		ioossre 12106	. . . . . . . . . . . 12 ⊢ (𝐵(,)𝐷) ⊆ ℝ
118	13, 117	sstri 3577	. . . . . . . . . . 11 ⊢ (𝐴 ∩ (𝐵(,)𝐷)) ⊆ ℝ
119	118	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)𝐷)) ⊆ ℝ)
120	19	snssd 4281	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} ⊆ ℝ)
121	119, 120	unssd 3751	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ⊆ ℝ)
122		reex 9906	. . . . . . . . . 10 ⊢ ℝ ∈ V
123	122	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ∈ V)
124		restabs 20779	. . . . . . . . 9 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))
125	116, 121, 123, 124	syl3anc 1318	. . . . . . . 8 ⊢ (𝜑 → (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))
126	115, 125	syl5eq 2656	. . . . . . 7 ⊢ (𝜑 → ((topGen‘ran (,)) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))
127	113, 126	eleqtrd 2690	. . . . . 6 ⊢ (𝜑 → (𝐵[,)𝐶) ∈ ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))
128		isopn3i 20696	. . . . . 6 ⊢ ((((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ Top ∧ (𝐵[,)𝐶) ∈ ((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘(𝐵[,)𝐶)) = (𝐵[,)𝐶))
129	35, 127, 128	syl2anc 691	. . . . 5 ⊢ (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘(𝐵[,)𝐶)) = (𝐵[,)𝐶))
130	27, 129	eqtr2d 2645	. . . 4 ⊢ (𝜑 → (𝐵[,)𝐶) = ((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘((𝐵(,)𝐶) ∪ {𝐵})))
131	24, 130	eleqtrd 2690	. . 3 ⊢ (𝜑 → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘((𝐵(,)𝐶) ∪ {𝐵})))
132	10, 12, 16, 17, 18, 131	limcres 23456	. 2 ⊢ (𝜑 → (((𝐹 ↾ (𝐵(,)𝐷)) ↾ (𝐵(,)𝐶)) limℂ 𝐵) = ((𝐹 ↾ (𝐵(,)𝐷)) limℂ 𝐵))
133	7, 132	eqtrd 2644	1 ⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐵) = ((𝐹 ↾ (𝐵(,)𝐷)) limℂ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  {csn 4125   class class class wbr 4583  ran crn 5039   ↾ cres 5040  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  -∞cmnf 9951  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954  (,)cioo 12046  [,)cico 12048   ↾_t crest 15904  TopOpenctopn 15905  topGenctg 15921  ℂ_fldccnfld 19567  Topctop 20517  intcnt 20631   lim_ℂ climc 23432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-mulr 15782  df-starv 15783  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-rest 15906  df-topn 15907  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-ntr 20634  df-cnp 20842  df-xms 21935  df-ms 21936  df-limc 23436

This theorem is referenced by:  fouriersw  39124