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		simpr	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to x\in \left(A\cup \left\{B\right\}\right)$$
30		elun	$$⊢x\in \left(A\cup \left\{B\right\}\right)\leftrightarrow \left(x\in A\vee x\in \left\{B\right\}\right)$$
31	29 30	sylib	$$⊢\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)$$
32	31	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)$$
33		elsni	$$⊢x\in \left\{B\right\}\to x=B$$
34	32 33	syl6	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to \left(\neg x\in A\to x=B\right)$$
35	34	con1d	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to \left(\neg x=B\to x\in A\right)$$
36	35	imp	$$⊢\left(\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\wedge \neg x=B\right)\to x\in A$$
37	28 36 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$$
38	27 37	ifclda	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to if\left(x=B,C,R\right)\in X$$
39	25	simprd	$$⊢\phi \to D\in Y$$
40	39	ad2antrr	$$⊢\left(\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\wedge x=B\right)\to D\in Y$$
41	28 36 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$$
42	40 41	ifclda	$$⊢\left(\phi \wedge x\in \left(A\cup \left\{B\right\}\right)\right)\to if\left(x=B,D,S\right)\in Y$$
43	38 42	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)$$
44		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)$$
45	13	a1i	$$⊢\phi \to K\in \mathrm{TopOn}\left(ℂ\right)$$
46		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⟶ℂ$$
47	20 45 9 46	syl3anc	$$⊢\phi \to H:X\times Y⟶ℂ$$
48	47	feqmptd	$$⊢\phi \to H=\left(y\in \left(X\times Y\right)⟼H\left(y\right)\right)$$
49		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)$$
50		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)$$
51		ovif12	$$⊢if\left(x=B,C,R\right)Hif\left(x=B,D,S\right)=if\left(x=B,CHD,RHS\right)$$
52	50 51	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)$$
53	49 52	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)$$
54	43 44 48 53	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)$$
55		eqid	$$⊢\left(x\in A⟼R\right)=\left(x\in A⟼R\right)$$
56	55 1	dmmptd	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼R\right)=A$$
57		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)$$
58	7 57	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)$$
59	58	simp2d	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼R\right)\subseteq ℂ$$
60	56 59	eqsstrrd	$$⊢\phi \to A\subseteq ℂ$$
61	58	simp3d	$$⊢\phi \to B\in ℂ$$
62	61	snssd	$$⊢\phi \to \left\{B\right\}\subseteq ℂ$$
63	60 62	unssd	$$⊢\phi \to A\cup \left\{B\right\}\subseteq ℂ$$
64		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)$$
65	13 63 64	sylancr	$$⊢\phi \to K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\in \mathrm{TopOn}\left(A\cup \left\{B\right\}\right)$$
66		ssun2	$$⊢\left\{B\right\}\subseteq A\cup \left\{B\right\}$$
67		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)$$
68	61 67	syl	$$⊢\phi \to \left(B\in \left(A\cup \left\{B\right\}\right)\leftrightarrow \left\{B\right\}\subseteq A\cup \left\{B\right\}\right)$$
69	66 68	mpbiri	$$⊢\phi \to B\in \left(A\cup \left\{B\right\}\right)$$
70	3	adantr	$$⊢\left(\phi \wedge x\in A\right)\to X\subseteq ℂ$$
71	70 1	sseldd	$$⊢\left(\phi \wedge x\in A\right)\to R\in ℂ$$
72		eqid	$$⊢K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)=K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)$$
73	60 61 71 72 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)$$
74	7 73	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)$$
75	4	adantr	$$⊢\left(\phi \wedge x\in A\right)\to Y\subseteq ℂ$$
76	75 2	sseldd	$$⊢\left(\phi \wedge x\in A\right)\to S\in ℂ$$
77	60 61 76 72 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)$$
78	8 77	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)$$
79	65 45 45 69 74 78	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)$$
80	15	topontopi	$$⊢K{\times }_{t}K\in \mathrm{Top}$$
81	80	a1i	$$⊢\phi \to K{\times }_{t}K\in \mathrm{Top}$$
82	43	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$$
83		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)$$
84	65 83	syl	$$⊢\phi \to A\cup \left\{B\right\}=\bigcup \left(K{\upharpoonright }_{𝑡}\left(A\cup \left\{B\right\}\right)\right)$$
85	84	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)$$
86	82 85	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$$
87		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)$$
88	15	toponunii	$$⊢ℂ\times ℂ=\bigcup \left(K{\times }_{t}K\right)$$
89	87 88	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)$$
90	81 86 17 89	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)$$
91	79 90	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)$$
92	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)$$
93	92	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)$$
94	91 93	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)$$
95		iftrue	$$⊢x=B\to if\left(x=B,C,R\right)=C$$
96		iftrue	$$⊢x=B\to if\left(x=B,D,S\right)=D$$
97	95 96	opeq12d	$$⊢x=B\to ⟨if\left(x=B,C,R\right),if\left(x=B,D,S\right)⟩=⟨C,D⟩$$
98		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)$$
99		opex	$$⊢⟨C,D⟩\in \mathrm{V}$$
100	97 98 99	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⟩$$
101	69 100	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⟩$$
102	101	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)$$
103	9 102	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)$$
104		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)$$
105	94 103 104	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)$$
106	54 105	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)$$
107	47	adantr	$$⊢\left(\phi \wedge x\in A\right)\to H:X\times Y⟶ℂ$$
108	107 1 2	fovrnd	$$⊢\left(\phi \wedge x\in A\right)\to RHS\in ℂ$$
109	60 61 108 72 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)$$
110	106 109	mpbird	$$⊢\phi \to CHD\in \left(\left(x\in A⟼RHS\right){lim}_{ℂ}B\right)$$