cncfiooicclem1

Description: A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding closed interval, if it has a finite right limit R in A and a finite left limit L in B . F can be complex-valued. This lemma assumes A < B , the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cncfiooicclem1.x	$⊢ Ⅎ x φ$
	cncfiooicclem1.g	$⊢ G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
	cncfiooicclem1.a	$⊢ φ \to A \in ℝ$
	cncfiooicclem1.b	$⊢ φ \to B \in ℝ$
	cncfiooicclem1.altb	$⊢ φ \to A < B$
	cncfiooicclem1.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
	cncfiooicclem1.l	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
	cncfiooicclem1.r	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
Assertion	cncfiooicclem1	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		cncfiooicclem1.x	$⊢ Ⅎ x φ$
2		cncfiooicclem1.g	$⊢ G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
3		cncfiooicclem1.a	$⊢ φ \to A \in ℝ$
4		cncfiooicclem1.b	$⊢ φ \to B \in ℝ$
5		cncfiooicclem1.altb	$⊢ φ \to A < B$
6		cncfiooicclem1.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
7		cncfiooicclem1.l	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
8		cncfiooicclem1.r	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
9		limccl	$⊢ F {lim}_{ℂ} A \subseteq ℂ$
10	9 8	sselid	$⊢ φ \to R \in ℂ$
11	10	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land x = A) \to R \in ℂ$
12		limccl	$⊢ F {lim}_{ℂ} B \subseteq ℂ$
13	12 7	sselid	$⊢ φ \to L \in ℂ$
14	13	ad3antrrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to L \in ℂ$
15		simplll	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to φ$
16		orel1	$⊢ \neg x = A \to ((x = A \lor x = B) \to x = B)$
17	16	con3dimp	$⊢ (\neg x = A \land \neg x = B) \to \neg (x = A \lor x = B)$
18		vex	$⊢ x \in V$
19	18	elpr	$⊢ x \in \{A, B\} \leftrightarrow (x = A \lor x = B)$
20	17 19	sylnibr	$⊢ (\neg x = A \land \neg x = B) \to \neg x \in \{A, B\}$
21	20	adantll	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to \neg x \in \{A, B\}$
22		simpllr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in [A, B]$
23	3	rexrd	$⊢ φ \to A \in ℝ^{*}$
24	15 23	syl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A \in ℝ^{*}$
25	4	rexrd	$⊢ φ \to B \in ℝ^{*}$
26	15 25	syl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to B \in ℝ^{*}$
27	3 4 5	ltled	$⊢ φ \to A \leq B$
28	15 27	syl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A \leq B$
29		prunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A, B) \cup \{A, B\} = [A, B]$
30	24 26 28 29	syl3anc	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to (A, B) \cup \{A, B\} = [A, B]$
31	22 30	eleqtrrd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in ((A, B) \cup \{A, B\})$
32		elun	$⊢ x \in ((A, B) \cup \{A, B\}) \leftrightarrow (x \in (A, B) \lor x \in \{A, B\})$
33	31 32	sylib	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to (x \in (A, B) \lor x \in \{A, B\})$
34		orel2	$⊢ \neg x \in \{A, B\} \to ((x \in (A, B) \lor x \in \{A, B\}) \to x \in (A, B))$
35	21 33 34	sylc	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in (A, B)$
36		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℂ \to F : (A, B) ⟶ ℂ$
37	6 36	syl	$⊢ φ \to F : (A, B) ⟶ ℂ$
38	37	ffvelcdmda	$⊢ (φ \land x \in (A, B)) \to F (x) \in ℂ$
39	15 35 38	syl2anc	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to F (x) \in ℂ$
40	14 39	ifclda	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to if (x = B, L, F (x)) \in ℂ$
41	11 40	ifclda	$⊢ (φ \land x \in [A, B]) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
42	1 41 2	fmptdf	$⊢ φ \to G : [A, B] ⟶ ℂ$
43		elun	$⊢ y \in ((A, B) \cup \{A, B\}) \leftrightarrow (y \in (A, B) \lor y \in \{A, B\})$
44	23 25 27 29	syl3anc	$⊢ φ \to (A, B) \cup \{A, B\} = [A, B]$
45	44	eleq2d	$⊢ φ \to (y \in ((A, B) \cup \{A, B\}) \leftrightarrow y \in [A, B])$
46	43 45	bitr3id	$⊢ φ \to ((y \in (A, B) \lor y \in \{A, B\}) \leftrightarrow y \in [A, B])$
47	46	biimpar	$⊢ (φ \land y \in [A, B]) \to (y \in (A, B) \lor y \in \{A, B\})$
48		ioossicc	$⊢ (A, B) \subseteq [A, B]$
49		fssres	$⊢ (G : [A, B] ⟶ ℂ \land (A, B) \subseteq [A, B]) \to ({G ↾}_{(A, B)}) : (A, B) ⟶ ℂ$
50	42 48 49	sylancl	$⊢ φ \to ({G ↾}_{(A, B)}) : (A, B) ⟶ ℂ$
51	50	feqmptd	$⊢ φ \to {G ↾}_{(A, B)} = (y \in (A, B) ⟼ ({G ↾}_{(A, B)}) (y))$
52		nfmpt1	$⊢ \underline{Ⅎ} x (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
53	2 52	nfcxfr	$⊢ \underline{Ⅎ} x G$
54		nfcv	$⊢ \underline{Ⅎ} x (A, B)$
55	53 54	nfres	$⊢ \underline{Ⅎ} x ({G ↾}_{(A, B)})$
56		nfcv	$⊢ \underline{Ⅎ} x y$
57	55 56	nffv	$⊢ \underline{Ⅎ} x ({G ↾}_{(A, B)}) (y)$
58		nfcv	$⊢ \underline{Ⅎ} y ({G ↾}_{(A, B)})$
59		nfcv	$⊢ \underline{Ⅎ} y x$
60	58 59	nffv	$⊢ \underline{Ⅎ} y ({G ↾}_{(A, B)}) (x)$
61		fveq2	$⊢ y = x \to ({G ↾}_{(A, B)}) (y) = ({G ↾}_{(A, B)}) (x)$
62	57 60 61	cbvmpt	$⊢ (y \in (A, B) ⟼ ({G ↾}_{(A, B)}) (y)) = (x \in (A, B) ⟼ ({G ↾}_{(A, B)}) (x))$
63	62	a1i	$⊢ φ \to (y \in (A, B) ⟼ ({G ↾}_{(A, B)}) (y)) = (x \in (A, B) ⟼ ({G ↾}_{(A, B)}) (x))$
64		fvres	$⊢ x \in (A, B) \to ({G ↾}_{(A, B)}) (x) = G (x)$
65	64	adantl	$⊢ (φ \land x \in (A, B)) \to ({G ↾}_{(A, B)}) (x) = G (x)$
66		simpr	$⊢ (φ \land x \in (A, B)) \to x \in (A, B)$
67	48 66	sselid	$⊢ (φ \land x \in (A, B)) \to x \in [A, B]$
68	10	adantr	$⊢ (φ \land x \in (A, B)) \to R \in ℂ$
69	13	ad2antrr	$⊢ ((φ \land x \in (A, B)) \land x = B) \to L \in ℂ$
70	38	adantr	$⊢ ((φ \land x \in (A, B)) \land \neg x = B) \to F (x) \in ℂ$
71	69 70	ifclda	$⊢ (φ \land x \in (A, B)) \to if (x = B, L, F (x)) \in ℂ$
72	68 71	ifcld	$⊢ (φ \land x \in (A, B)) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
73	2	fvmpt2	$⊢ (x \in [A, B] \land if (x = A, R, if (x = B, L, F (x))) \in ℂ) \to G (x) = if (x = A, R, if (x = B, L, F (x)))$
74	67 72 73	syl2anc	$⊢ (φ \land x \in (A, B)) \to G (x) = if (x = A, R, if (x = B, L, F (x)))$
75		elioo4g	$⊢ x \in (A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ) \land (A < x \land x < B))$
76	75	biimpi	$⊢ x \in (A, B) \to ((A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ) \land (A < x \land x < B))$
77	76	simpld	$⊢ x \in (A, B) \to (A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ)$
78	77	simp1d	$⊢ x \in (A, B) \to A \in ℝ^{*}$
79		elioore	$⊢ x \in (A, B) \to x \in ℝ$
80	79	rexrd	$⊢ x \in (A, B) \to x \in ℝ^{*}$
81		eliooord	$⊢ x \in (A, B) \to (A < x \land x < B)$
82	81	simpld	$⊢ x \in (A, B) \to A < x$
83		xrltne	$⊢ (A \in ℝ^{} \land x \in ℝ^{} \land A < x) \to x \neq A$
84	78 80 82 83	syl3anc	$⊢ x \in (A, B) \to x \neq A$
85	84	adantl	$⊢ (φ \land x \in (A, B)) \to x \neq A$
86	85	neneqd	$⊢ (φ \land x \in (A, B)) \to \neg x = A$
87	86	iffalsed	$⊢ (φ \land x \in (A, B)) \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
88	81	simprd	$⊢ x \in (A, B) \to x < B$
89	79 88	ltned	$⊢ x \in (A, B) \to x \neq B$
90	89	neneqd	$⊢ x \in (A, B) \to \neg x = B$
91	90	iffalsed	$⊢ x \in (A, B) \to if (x = B, L, F (x)) = F (x)$
92	91	adantl	$⊢ (φ \land x \in (A, B)) \to if (x = B, L, F (x)) = F (x)$
93	87 92	eqtrd	$⊢ (φ \land x \in (A, B)) \to if (x = A, R, if (x = B, L, F (x))) = F (x)$
94	65 74 93	3eqtrd	$⊢ (φ \land x \in (A, B)) \to ({G ↾}_{(A, B)}) (x) = F (x)$
95	1 94	mpteq2da	$⊢ φ \to (x \in (A, B) ⟼ ({G ↾}_{(A, B)}) (x)) = (x \in (A, B) ⟼ F (x))$
96	51 63 95	3eqtrd	$⊢ φ \to {G ↾}_{(A, B)} = (x \in (A, B) ⟼ F (x))$
97	37	feqmptd	$⊢ φ \to F = (x \in (A, B) ⟼ F (x))$
98		ioosscn	$⊢ (A, B) \subseteq ℂ$
99	98	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
100		ssid	$⊢ ℂ \subseteq ℂ$
101		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
102		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)$
103	101	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
104		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
105	104	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
106	103 105	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
107	106	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
108	101 102 107	cncfcn	$⊢ ((A, B) \subseteq ℂ \land ℂ \subseteq ℂ) \to (A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})$
109	99 100 108	sylancl	$⊢ φ \to (A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})$
110	6 97 109	3eltr3d	$⊢ φ \to (x \in (A, B) ⟼ F (x)) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld}))$
111	96 110	eqeltrd	$⊢ φ \to {G ↾}_{(A, B)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld}))$
112	104	restuni	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (A, B) \subseteq ℂ) \to (A, B) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
113	103 98 112	mp2an	$⊢ (A, B) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B))$
114	113	cncnpi	$⊢ ({G ↾}_{(A, B)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})) \land y \in (A, B)) \to {G ↾}_{(A, B)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (y)$
115	111 114	sylan	$⊢ (φ \land y \in (A, B)) \to {G ↾}_{(A, B)} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (y)$
116	103	a1i	$⊢ (φ \land y \in (A, B)) \to TopOpen (ℂ_{fld}) \in Top$
117	48	a1i	$⊢ (φ \land y \in (A, B)) \to (A, B) \subseteq [A, B]$
118		ovex	$⊢ [A, B] \in V$
119	118	a1i	$⊢ (φ \land y \in (A, B)) \to [A, B] \in V$
120		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (A, B) \subseteq [A, B] \land [A, B] \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ↾_{𝑡} (A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)$
121	116 117 119 120	syl3anc	$⊢ (φ \land y \in (A, B)) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ↾_{𝑡} (A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)$
122	121	eqcomd	$⊢ (φ \land y \in (A, B)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) = (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ↾_{𝑡} (A, B)$
123	122	oveq1d	$⊢ (φ \land y \in (A, B)) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld}) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})$
124	123	fveq1d	$⊢ (φ \land y \in (A, B)) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (y) = (((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (y)$
125	115 124	eleqtrd	$⊢ (φ \land y \in (A, B)) \to {G ↾}_{(A, B)} \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (y)$
126		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [A, B] \in V) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] \in Top$
127	103 118 126	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] \in Top$
128	127	a1i	$⊢ (φ \land y \in (A, B)) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] \in Top$
129	48	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
130	3 4	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
131		ax-resscn	$⊢ ℝ \subseteq ℂ$
132	130 131	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
133	104	restuni	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [A, B] \subseteq ℂ) \to [A, B] = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B])$
134	103 132 133	sylancr	$⊢ φ \to [A, B] = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B])$
135	129 134	sseqtrd	$⊢ φ \to (A, B) \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B])$
136	135	adantr	$⊢ (φ \land y \in (A, B)) \to (A, B) \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B])$
137		retop	$⊢ topGen (ran (.)) \in Top$
138	137	a1i	$⊢ (φ \land y \in (A, B)) \to topGen (ran (.)) \in Top$
139		ioossre	$⊢ (A, B) \subseteq ℝ$
140		difss	$⊢ ℝ ∖ [A, B] \subseteq ℝ$
141	139 140	unssi	$⊢ (A, B) \cup (ℝ ∖ [A, B]) \subseteq ℝ$
142	141	a1i	$⊢ (φ \land y \in (A, B)) \to (A, B) \cup (ℝ ∖ [A, B]) \subseteq ℝ$
143		ssun1	$⊢ (A, B) \subseteq (A, B) \cup (ℝ ∖ [A, B])$
144	143	a1i	$⊢ (φ \land y \in (A, B)) \to (A, B) \subseteq (A, B) \cup (ℝ ∖ [A, B])$
145		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
146	145	ntrss	$⊢ (topGen (ran (.)) \in Top \land (A, B) \cup (ℝ ∖ [A, B]) \subseteq ℝ \land (A, B) \subseteq (A, B) \cup (ℝ ∖ [A, B])) \to int (topGen (ran (.))) ((A, B)) \subseteq int (topGen (ran (.))) ((A, B) \cup (ℝ ∖ [A, B]))$
147	138 142 144 146	syl3anc	$⊢ (φ \land y \in (A, B)) \to int (topGen (ran (.))) ((A, B)) \subseteq int (topGen (ran (.))) ((A, B) \cup (ℝ ∖ [A, B]))$
148		simpr	$⊢ (φ \land y \in (A, B)) \to y \in (A, B)$
149		ioontr	$⊢ int (topGen (ran (.))) ((A, B)) = (A, B)$
150	148 149	eleqtrrdi	$⊢ (φ \land y \in (A, B)) \to y \in int (topGen (ran (.))) ((A, B))$
151	147 150	sseldd	$⊢ (φ \land y \in (A, B)) \to y \in int (topGen (ran (.))) ((A, B) \cup (ℝ ∖ [A, B]))$
152	48 148	sselid	$⊢ (φ \land y \in (A, B)) \to y \in [A, B]$
153	151 152	elind	$⊢ (φ \land y \in (A, B)) \to y \in (int (topGen (ran (.))) ((A, B) \cup (ℝ ∖ [A, B])) \cap [A, B])$
154	130	adantr	$⊢ (φ \land y \in (A, B)) \to [A, B] \subseteq ℝ$
155		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [A, B] = topGen (ran (.)) ↾_{𝑡} [A, B]$
156	145 155	restntr	$⊢ (topGen (ran (.)) \in Top \land [A, B] \subseteq ℝ \land (A, B) \subseteq [A, B]) \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) ((A, B)) = int (topGen (ran (.))) ((A, B) \cup (ℝ ∖ [A, B])) \cap [A, B]$
157	138 154 117 156	syl3anc	$⊢ (φ \land y \in (A, B)) \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) ((A, B)) = int (topGen (ran (.))) ((A, B) \cup (ℝ ∖ [A, B])) \cap [A, B]$
158	153 157	eleqtrrd	$⊢ (φ \land y \in (A, B)) \to y \in int (topGen (ran (.)) ↾_{𝑡} [A, B]) ((A, B))$
159	101	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
160	159	a1i	$⊢ φ \to topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
161	160	oveq1d	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [A, B] = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [A, B]$
162	103	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
163		reex	$⊢ ℝ \in V$
164	163	a1i	$⊢ φ \to ℝ \in V$
165		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [A, B] \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]$
166	162 130 164 165	syl3anc	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]$
167	161 166	eqtrd	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]$
168	167	fveq2d	$⊢ φ \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B])$
169	168	fveq1d	$⊢ φ \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) ((A, B)) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ((A, B))$
170	169	adantr	$⊢ (φ \land y \in (A, B)) \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) ((A, B)) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ((A, B))$
171	158 170	eleqtrd	$⊢ (φ \land y \in (A, B)) \to y \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ((A, B))$
172	134	feq2d	$⊢ φ \to (G : [A, B] ⟶ ℂ \leftrightarrow G : ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ⟶ ℂ)$
173	42 172	mpbid	$⊢ φ \to G : ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ⟶ ℂ$
174	173	adantr	$⊢ (φ \land y \in (A, B)) \to G : ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ⟶ ℂ$
175		eqid	$⊢ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B])$
176	175 104	cnprest	$⊢ ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] \in Top \land (A, B) \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B])) \land (y \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ((A, B)) \land G : ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ⟶ ℂ)) \to (G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y) \leftrightarrow {G ↾}_{(A, B)} \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (y))$
177	128 136 171 174 176	syl22anc	$⊢ (φ \land y \in (A, B)) \to (G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y) \leftrightarrow {G ↾}_{(A, B)} \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (y))$
178	125 177	mpbird	$⊢ (φ \land y \in (A, B)) \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
179		elpri	$⊢ y \in \{A, B\} \to (y = A \lor y = B)$
180		iftrue	$⊢ x = A \to if (x = A, R, if (x = B, L, F (x))) = R$
181		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
182	23 25 27 181	syl3anc	$⊢ φ \to A \in [A, B]$
183	2 180 182 8	fvmptd3	$⊢ φ \to G (A) = R$
184	97	eqcomd	$⊢ φ \to (x \in (A, B) ⟼ F (x)) = F$
185	96 184	eqtr2d	$⊢ φ \to F = {G ↾}_{(A, B)}$
186	185	oveq1d	$⊢ φ \to F {lim}_{ℂ} A = ({G ↾}_{(A, B)}) {lim}_{ℂ} A$
187	8 186	eleqtrd	$⊢ φ \to R \in (({G ↾}_{(A, B)}) {lim}_{ℂ} A)$
188	3 4 5 42	limciccioolb	$⊢ φ \to ({G ↾}_{(A, B)}) {lim}_{ℂ} A = G {lim}_{ℂ} A$
189	187 188	eleqtrd	$⊢ φ \to R \in (G {lim}_{ℂ} A)$
190	183 189	eqeltrd	$⊢ φ \to G (A) \in (G {lim}_{ℂ} A)$
191		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]$
192	101 191	cnplimc	$⊢ ([A, B] \subseteq ℂ \land A \in [A, B]) \to (G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (A) \leftrightarrow (G : [A, B] ⟶ ℂ \land G (A) \in (G {lim}_{ℂ} A)))$
193	132 182 192	syl2anc	$⊢ φ \to (G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (A) \leftrightarrow (G : [A, B] ⟶ ℂ \land G (A) \in (G {lim}_{ℂ} A)))$
194	42 190 193	mpbir2and	$⊢ φ \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (A)$
195	194	adantr	$⊢ (φ \land y = A) \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (A)$
196		fveq2	$⊢ y = A \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (A)$
197	196	eqcomd	$⊢ y = A \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (A) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
198	197	adantl	$⊢ (φ \land y = A) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (A) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
199	195 198	eleqtrd	$⊢ (φ \land y = A) \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
200	180	adantl	$⊢ (x = B \land x = A) \to if (x = A, R, if (x = B, L, F (x))) = R$
201		eqtr2	$⊢ (x = B \land x = A) \to B = A$
202		iftrue	$⊢ B = A \to if (B = A, R, if (B = B, L, F (B))) = R$
203	202	eqcomd	$⊢ B = A \to R = if (B = A, R, if (B = B, L, F (B)))$
204	201 203	syl	$⊢ (x = B \land x = A) \to R = if (B = A, R, if (B = B, L, F (B)))$
205	200 204	eqtrd	$⊢ (x = B \land x = A) \to if (x = A, R, if (x = B, L, F (x))) = if (B = A, R, if (B = B, L, F (B)))$
206		iffalse	$⊢ \neg x = A \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
207	206	adantl	$⊢ (x = B \land \neg x = A) \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
208		iftrue	$⊢ x = B \to if (x = B, L, F (x)) = L$
209	208	adantr	$⊢ (x = B \land \neg x = A) \to if (x = B, L, F (x)) = L$
210		df-ne	$⊢ x \neq A \leftrightarrow \neg x = A$
211		pm13.18	$⊢ (x = B \land x \neq A) \to B \neq A$
212	210 211	sylan2br	$⊢ (x = B \land \neg x = A) \to B \neq A$
213	212	neneqd	$⊢ (x = B \land \neg x = A) \to \neg B = A$
214	213	iffalsed	$⊢ (x = B \land \neg x = A) \to if (B = A, R, if (B = B, L, F (B))) = if (B = B, L, F (B))$
215		eqid	$⊢ B = B$
216	215	iftruei	$⊢ if (B = B, L, F (B)) = L$
217	214 216	eqtr2di	$⊢ (x = B \land \neg x = A) \to L = if (B = A, R, if (B = B, L, F (B)))$
218	207 209 217	3eqtrd	$⊢ (x = B \land \neg x = A) \to if (x = A, R, if (x = B, L, F (x))) = if (B = A, R, if (B = B, L, F (B)))$
219	205 218	pm2.61dan	$⊢ x = B \to if (x = A, R, if (x = B, L, F (x))) = if (B = A, R, if (B = B, L, F (B)))$
220	4	leidd	$⊢ φ \to B \leq B$
221	3 4 4 27 220	eliccd	$⊢ φ \to B \in [A, B]$
222	216 13	eqeltrid	$⊢ φ \to if (B = B, L, F (B)) \in ℂ$
223	10 222	ifcld	$⊢ φ \to if (B = A, R, if (B = B, L, F (B))) \in ℂ$
224	2 219 221 223	fvmptd3	$⊢ φ \to G (B) = if (B = A, R, if (B = B, L, F (B)))$
225	3 5	gtned	$⊢ φ \to B \neq A$
226	225	neneqd	$⊢ φ \to \neg B = A$
227	226	iffalsed	$⊢ φ \to if (B = A, R, if (B = B, L, F (B))) = if (B = B, L, F (B))$
228	216	a1i	$⊢ φ \to if (B = B, L, F (B)) = L$
229	224 227 228	3eqtrd	$⊢ φ \to G (B) = L$
230	185	oveq1d	$⊢ φ \to F {lim}_{ℂ} B = ({G ↾}_{(A, B)}) {lim}_{ℂ} B$
231	7 230	eleqtrd	$⊢ φ \to L \in (({G ↾}_{(A, B)}) {lim}_{ℂ} B)$
232	3 4 5 42	limcicciooub	$⊢ φ \to ({G ↾}_{(A, B)}) {lim}_{ℂ} B = G {lim}_{ℂ} B$
233	231 232	eleqtrd	$⊢ φ \to L \in (G {lim}_{ℂ} B)$
234	229 233	eqeltrd	$⊢ φ \to G (B) \in (G {lim}_{ℂ} B)$
235	101 191	cnplimc	$⊢ ([A, B] \subseteq ℂ \land B \in [A, B]) \to (G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (B) \leftrightarrow (G : [A, B] ⟶ ℂ \land G (B) \in (G {lim}_{ℂ} B)))$
236	132 221 235	syl2anc	$⊢ φ \to (G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (B) \leftrightarrow (G : [A, B] ⟶ ℂ \land G (B) \in (G {lim}_{ℂ} B)))$
237	42 234 236	mpbir2and	$⊢ φ \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (B)$
238	237	adantr	$⊢ (φ \land y = B) \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (B)$
239		fveq2	$⊢ y = B \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (B)$
240	239	eqcomd	$⊢ y = B \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (B) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
241	240	adantl	$⊢ (φ \land y = B) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (B) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
242	238 241	eleqtrd	$⊢ (φ \land y = B) \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
243	199 242	jaodan	$⊢ (φ \land (y = A \lor y = B)) \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
244	179 243	sylan2	$⊢ (φ \land y \in \{A, B\}) \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
245	178 244	jaodan	$⊢ (φ \land (y \in (A, B) \lor y \in \{A, B\})) \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
246	47 245	syldan	$⊢ (φ \land y \in [A, B]) \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
247	246	ralrimiva	$⊢ φ \to \forall y \in [A, B] G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)$
248	101	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
249		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land [A, B] \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] \in TopOn ([A, B])$
250	248 132 249	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] \in TopOn ([A, B])$
251		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] \in TopOn ([A, B]) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to (G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) Cn TopOpen (ℂ_{fld})) \leftrightarrow (G : [A, B] ⟶ ℂ \land \forall y \in [A, B] G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)))$
252	250 248 251	sylancl	$⊢ φ \to (G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) Cn TopOpen (ℂ_{fld})) \leftrightarrow (G : [A, B] ⟶ ℂ \land \forall y \in [A, B] G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) CnP TopOpen (ℂ_{fld})) (y)))$
253	42 247 252	mpbir2and	$⊢ φ \to G \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) Cn TopOpen (ℂ_{fld}))$
254	101 191 107	cncfcn	$⊢ ([A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to [A, B] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) Cn TopOpen (ℂ_{fld})$
255	132 100 254	sylancl	$⊢ φ \to [A, B] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) Cn TopOpen (ℂ_{fld})$
256	253 255	eleqtrrd	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem cncfiooicclem1

Proof