Theorem limccnp2

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	limccnp2.r	$$⊢\left(\phi \wedge x\in A\right)\to R\in X$$
	limccnp2.s	$$⊢\left(\phi \wedge x\in A\right)\to S\in Y$$
	limccnp2.x	$$⊢\phi \to X\subseteq ℂ$$
	limccnp2.y	$$⊢\phi \to Y\subseteq ℂ$$
	limccnp2.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	limccnp2.j	$$⊢J=\left(K{\times }_{t}K\right){\upharpoonright }_{𝑡}\left(X\times Y\right)$$
	limccnp2.c	$$⊢\phi \to C\in \left(\left(x\in A⟼R\right){lim}_{ℂ}B\right)$$
	limccnp2.d	$$⊢\phi \to D\in \left(\left(x\in A⟼S\right){lim}_{ℂ}B\right)$$
	limccnp2.h	$$⊢\phi \to H\in \left(J\mathrm{CnP}K\right)\left(⟨C,D⟩\right)$$
Assertion	limccnp2	$$⊢\phi \to CHD\in \left(\left(x\in A⟼RHS\right){lim}_{ℂ}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		limccnp2.r	$$⊢\left(\phi \wedge x\in A\right)\to R\in X$$
2		limccnp2.s	$$⊢\left(\phi \wedge x\in A\right)\to S\in Y$$
3		limccnp2.x	$$⊢\phi \to X\subseteq ℂ$$
4		limccnp2.y	$$⊢\phi \to Y\subseteq ℂ$$
5		limccnp2.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
6		limccnp2.j	$$⊢J=\left(K{\times }_{t}K\right){\upharpoonright }_{𝑡}\left(X\times Y\right)$$
7		limccnp2.c	$$⊢\phi \to C\in \left(\left(x\in A⟼R\right){lim}_{ℂ}B\right)$$
8		limccnp2.d	$$⊢\phi \to D\in \left(\left(x\in A⟼S\right){lim}_{ℂ}B\right)$$
9		limccnp2.h	$$⊢\phi \to H\in \left(J\mathrm{CnP}K\right)\left(⟨C,D⟩\right)$$
10		eqid	$$⊢\bigcup J=\bigcup J$$
11	10	cnprcl	$$⊢H\in \left(J\mathrm{CnP}K\right)\left(⟨C,D⟩\right)\to ⟨C,D⟩\in \bigcup J$$
12	9 11	syl	$$⊢\phi \to ⟨C,D⟩\in \bigcup J$$
13	5	cnfldtopon	$$⊢K\in \mathrm{TopOn}\left(ℂ\right)$$
14		txtopon	$$⊢\left(K\in \mathrm{TopOn}\left(ℂ\right)\wedge K\in \mathrm{TopOn}\left(ℂ\right)\right)\to K{\times }_{t}K\in \mathrm{TopOn}\left(ℂ\times ℂ\right)$$
15	13 13 14	mp2an	$$⊢K{\times }_{t}K\in \mathrm{TopOn}\left(ℂ\times ℂ\right)$$
16		xpss12	$$⊢\left(X\subseteq ℂ\wedge Y\subseteq ℂ\right)\to X\times Y\subseteq ℂ\times ℂ$$
17	3 4 16	syl2anc	$$⊢\phi \to X\times Y\subseteq ℂ\times ℂ$$
18		resttopon	$$⊢\left(K{\times }_{t}K\in \mathrm{TopOn}\left(ℂ\times ℂ\right)\wedge X\times Y\subseteq ℂ\times ℂ\right)\to \left(K{\times }_{t}K\right){\upharpoonright }_{𝑡}\left(X\times Y\right)\in \mathrm{TopOn}\left(X\times Y\right)$$
19	15 17 18	sylancr	$$⊢\phi \to \left(K{\times }_{t}K\right){\upharpoonright }_{𝑡}\left(X\times Y\right)\in \mathrm{TopOn}\left(X\times Y\right)$$
20	6 19	eqeltrid	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\times Y\right)$$
21		toponuni	$$⊢J\in \mathrm{TopOn}\left(X\times Y\right)\to X\times Y=\bigcup J$$
22	20 21	syl	$$⊢\phi \to X\times Y=\bigcup J$$
23	12 22	eleqtrrd	$$⊢\phi \to ⟨C,D⟩\in \left(X\times Y\right)$$
24		opelxp	$$⊢⟨C,D⟩\in \left(X\times Y\right)\leftrightarrow \left(C\in X\wedge D\in Y\right)$$
25	23 24	sylib	$$⊢\phi \to \left(C\in X\wedge D\in Y\right)$$
26	25	simpld	$$⊢\phi \to C\in X$$
27	26	ad2antrr	$$⊢\left(\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\wedge x=B\right)\to C\in X$$
28		simpll	$$⊢\left(\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\wedge \neg x=B\right)\to \phi$$
29		elun	$$⊢x\in \left(A\cup \left\{B\right\}\right)\leftrightarrow \left(x\in A\vee x\in \left\{B\right\}\right)$$
30	29	bilani	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to \left(x\in A\vee x\in \left\{B\right\}\right)$$
31	30	ord	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to \left(\neg x\in A\to x\in \left\{B\right\}\right)$$
32		elsni	$$⊢x\in \left\{B\right\}\to x=B$$
33	31 32	syl6	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to \left(\neg x\in A\to x=B\right)$$
34	33	con1d	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to \left(\neg x=B\to x\in A\right)$$
35	34	imp	$$⊢\left(\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\wedge \neg x=B\right)\to x\in A$$
36	28 35 1	syl2anc	$$⊢\left(\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\wedge \neg x=B\right)\to R\in X$$
37	27 36	ifclda	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to if\left(x=B,C,R\right)\in X$$
38	25	simprd	$$⊢\phi \to D\in Y$$
39	38	ad2antrr	$$⊢\left(\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\wedge x=B\right)\to D\in Y$$
40	28 35 2	syl2anc	$$⊢\left(\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\wedge \neg x=B\right)\to S\in Y$$
41	39 40	ifclda	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to if\left(x=B,D,S\right)\in Y$$
42	37 41	opelxpd	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to ⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\in \left(X\times Y\right)$$
43		eqidd	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)=\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)$$
44	13	a1i	$$⊢\phi \to K\in \mathrm{TopOn}\left(ℂ\right)$$
45		cnpf2	$$⊢\left(J\in \mathrm{TopOn}\left(X\times Y\right)\wedge K\in \mathrm{TopOn}\left(ℂ\right)\wedge H\in \left(J\mathrm{CnP}K\right)\left(⟨C,D⟩\right)\right)\to H:X\times Y⟶ℂ$$
46	20 44 9 45	syl3anc	$$⊢\phi \to H:X\times Y⟶ℂ$$
47	46	feqmptd	$$⊢\phi \to H=\left(y\in \left(X\times Y\right)⟼H\left(y\right)\right)$$
48		fveq2	$$⊢y=⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\to H\left(y\right)=H\left(⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)$$
49		df-ov	$$⊢if\left(x=B,C,R\right)Hif\left(x=B,D,S\right)=H\left(⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)$$
50		ovif12	$$⊢if\left(x=B,C,R\right)Hif\left(x=B,D,S\right)=if\left(x=B,CHD,RHS\right)$$
51	49 50	eqtr3i	$$⊢H\left(⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)=if\left(x=B,CHD,RHS\right)$$
52	48 51	eqtrdi	$$⊢y=⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\to H\left(y\right)=if\left(x=B,CHD,RHS\right)$$
53	42 43 47 52	fmptco	$$⊢\phi \to H\circ \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)=\left(x\in \left(A\cup \left\{B\right\}\right)⟼if\left(x=B,CHD,RHS\right)\right)$$
54		eqid	$$⊢\left(x\in A⟼R\right)=\left(x\in A⟼R\right)$$
55	54 1	dmmptd	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼R\right)=A$$
56		limcrcl	$$⊢C\in \left(\left(x\in A⟼R\right){lim}_{ℂ}B\right)\to \left(\left(x\in A⟼R\right):\mathrm{dom}\left(x\in A⟼R\right)⟶ℂ\wedge \mathrm{dom}\left(x\in A⟼R\right)\subseteq ℂ\wedge B\in ℂ\right)$$
57	7 56	syl	$$⊢\phi \to \left(\left(x\in A⟼R\right):\mathrm{dom}\left(x\in A⟼R\right)⟶ℂ\wedge \mathrm{dom}\left(x\in A⟼R\right)\subseteq ℂ\wedge B\in ℂ\right)$$
58	57	simp2d	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼R\right)\subseteq ℂ$$
59	55 58	eqsstrrd	$$⊢\phi \to A\subseteq ℂ$$
60	57	simp3d	$$⊢\phi \to B\in ℂ$$
61	60	snssd	$$⊢\phi \to \left\{B\right\}\subseteq ℂ$$
62	59 61	unssd	$$⊢\phi \to A\cup \left\{B\right\}\subseteq ℂ$$
63		resttopon	$$⊢\left(K\in \mathrm{TopOn}\left(ℂ\right)\wedge A\cup \left\{B\right\}\subseteq ℂ\right)\to K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\in \mathrm{TopOn}\left(A\cup \left\{B\right\}\right)$$
64	13 62 63	sylancr	$$⊢\phi \to K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\in \mathrm{TopOn}\left(A\cup \left\{B\right\}\right)$$
65		ssun2	$$⊢\left\{B\right\}\subseteq A\cup \left\{B\right\}$$
66		snssg	$$⊢B\in ℂ\to \left(B\in \left(A\cup \left\{B\right\}\right)\leftrightarrow \left\{B\right\}\subseteq A\cup \left\{B\right\}\right)$$
67	60 66	syl	$$⊢\phi \to \left(B\in \left(A\cup \left\{B\right\}\right)\leftrightarrow \left\{B\right\}\subseteq A\cup \left\{B\right\}\right)$$
68	65 67	mpbiri	$$⊢\phi \to B\in \left(A\cup \left\{B\right\}\right)$$
69	3	adantr	$$⊢\left(\phi \wedge x\in A\right)\to X\subseteq ℂ$$
70	69 1	sseldd	$$⊢\left(\phi \wedge x\in A\right)\to R\in ℂ$$
71		eqid	$$⊢K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)=K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)$$
72	59 60 70 71 5	limcmpt	$$⊢\phi \to \left(C\in \left(\left(x\in A⟼R\right){lim}_{ℂ}B\right)\leftrightarrow \left(x\in \left(A\cup \left\{B\right\}\right)⟼if\left(x=B,C,R\right)\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}K\right)\left(B\right)\right)$$
73	7 72	mpbid	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼if\left(x=B,C,R\right)\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}K\right)\left(B\right)$$
74	4	adantr	$$⊢\left(\phi \wedge x\in A\right)\to Y\subseteq ℂ$$
75	74 2	sseldd	$$⊢\left(\phi \wedge x\in A\right)\to S\in ℂ$$
76	59 60 75 71 5	limcmpt	$$⊢\phi \to \left(D\in \left(\left(x\in A⟼S\right){lim}_{ℂ}B\right)\leftrightarrow \left(x\in \left(A\cup \left\{B\right\}\right)⟼if\left(x=B,D,S\right)\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}K\right)\left(B\right)\right)$$
77	8 76	mpbid	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼if\left(x=B,D,S\right)\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}K\right)\left(B\right)$$
78	64 44 44 68 73 77	txcnp	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}\left(K{\times }_{t}K\right)\right)\left(B\right)$$
79	15	topontopi	$$⊢K{\times }_{t}K\in \mathrm{Top}$$
80	79	a1i	$$⊢\phi \to K{\times }_{t}K\in \mathrm{Top}$$
81	42	fmpttd	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right):A\cup \left\{B\right\}⟶X\times Y$$
82		toponuni	$$⊢K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\in \mathrm{TopOn}\left(A\cup \left\{B\right\}\right)\to A\cup \left\{B\right\}=\bigcup \left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)$$
83	64 82	syl	$$⊢\phi \to A\cup \left\{B\right\}=\bigcup \left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)$$
84	83	feq2d	$$⊢\phi \to \left(\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right):A\cup \left\{B\right\}⟶X\times Y\leftrightarrow \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right):\bigcup \left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)⟶X\times Y\right)$$
85	81 84	mpbid	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right):\bigcup \left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)⟶X\times Y$$
86		eqid	$$⊢\bigcup \left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)=\bigcup \left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)$$
87	15	toponunii	$$⊢ℂ\times ℂ=\bigcup \left(K{\times }_{t}K\right)$$
88	86 87	cnprest2	$$⊢\left(K{\times }_{t}K\in \mathrm{Top}\wedge \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right):\bigcup \left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)⟶X\times Y\wedge X\times Y\subseteq ℂ\times ℂ\right)\to \left(\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}\left(K{\times }_{t}K\right)\right)\left(B\right)\leftrightarrow \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}\left(\left(K{\times }_{t}K\right){\upharpoonright }_{𝑡}\left(X\times Y\right)\right)\right)\left(B\right)\right)$$
89	80 85 17 88	syl3anc	$$⊢\phi \to \left(\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}\left(K{\times }_{t}K\right)\right)\left(B\right)\leftrightarrow \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}\left(\left(K{\times }_{t}K\right){\upharpoonright }_{𝑡}\left(X\times Y\right)\right)\right)\left(B\right)\right)$$
90	78 89	mpbid	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}\left(\left(K{\times }_{t}K\right){\upharpoonright }_{𝑡}\left(X\times Y\right)\right)\right)\left(B\right)$$
91	6	oveq2i	$$⊢\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}J=\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}\left(\left(K{\times }_{t}K\right){\upharpoonright }_{𝑡}\left(X\times Y\right)\right)$$
92	91	fveq1i	$$⊢\left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}J\right)\left(B\right)=\left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}\left(\left(K{\times }_{t}K\right){\upharpoonright }_{𝑡}\left(X\times Y\right)\right)\right)\left(B\right)$$
93	90 92	eleqtrrdi	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}J\right)\left(B\right)$$
94		iftrue	$$⊢x=B\to if\left(x=B,C,R\right)=C$$
95		iftrue	$$⊢x=B\to if\left(x=B,D,S\right)=D$$
96	94 95	opeq12d	$$⊢x=B\to ⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩=⟨C,D⟩$$
97		eqid	$$⊢\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)=\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)$$
98		opex	$$⊢⟨C,D⟩\in \mathrm{V}$$
99	96 97 98	fvmpt	$$⊢B\in \left(A\cup \left\{B\right\}\right)\to \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\left(B\right)=⟨C,D⟩$$
100	68 99	syl	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\left(B\right)=⟨C,D⟩$$
101	100	fveq2d	$$⊢\phi \to \left(J\mathrm{CnP}K\right)\left(\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\left(B\right)\right)=\left(J\mathrm{CnP}K\right)\left(⟨C,D⟩\right)$$
102	9 101	eleqtrrd	$$⊢\phi \to H\in \left(J\mathrm{CnP}K\right)\left(\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\left(B\right)\right)$$
103		cnpco	$$⊢\left(\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}J\right)\left(B\right)\wedge H\in \left(J\mathrm{CnP}K\right)\left(\left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\left(B\right)\right)\right)\to H\circ \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}K\right)\left(B\right)$$
104	93 102 103	syl2anc	$$⊢\phi \to H\circ \left(x\in \left(A\cup \left\{B\right\}\right)⟼⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}K\right)\left(B\right)$$
105	53 104	eqeltrrd	$$⊢\phi \to \left(x\in \left(A\cup \left\{B\right\}\right)⟼if\left(x=B,CHD,RHS\right)\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}K\right)\left(B\right)$$
106	46	adantr	$$⊢\left(\phi \wedge x\in A\right)\to H:X\times Y⟶ℂ$$
107	106 1 2	fovcdmd	$$⊢\left(\phi \wedge x\in A\right)\to RHS\in ℂ$$
108	59 60 107 71 5	limcmpt	$$⊢\phi \to \left(CHD\in \left(\left(x\in A⟼RHS\right){lim}_{ℂ}B\right)\leftrightarrow \left(x\in \left(A\cup \left\{B\right\}\right)⟼if\left(x=B,CHD,RHS\right)\right)\in \left(\left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)\mathrm{CnP}K\right)\left(B\right)\right)$$
109	105 108	mpbird	$$⊢\phi \to CHD\in \left(\left(x\in A⟼RHS\right){lim}_{ℂ}B\right)$$