Theorem dvcnvrelem2

Description: Lemma for dvcnvre . (Contributed by Mario Carneiro, 19-Feb-2015) (Revised by Mario Carneiro, 8-Sep-2015)

	Ref	Expression
Hypotheses	dvcnvre.f	$$⊢\phi \to F:X\underset{cn}{⟶}ℝ$$
	dvcnvre.d	$$⊢\phi \to \mathrm{dom}{F}_{ℝ}^{\prime }=X$$
	dvcnvre.z	$$⊢\phi \to \neg 0\in \mathrm{ran}{F}_{ℝ}^{\prime }$$
	dvcnvre.1	$$⊢\phi \to F:X\underset{1-1\; onto}{⟶}Y$$
	dvcnvre.c	$$⊢\phi \to C\in X$$
	dvcnvre.r	$$⊢\phi \to R\in {ℝ}^{+}$$
	dvcnvre.s	$$⊢\phi \to \left[C-R,C+R\right]\subseteq X$$
	dvcnvre.t	$$⊢T=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	dvcnvre.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	dvcnvre.m	$$⊢M=J{\upharpoonright }_{𝑡}X$$
	dvcnvre.n	$$⊢N=J{\upharpoonright }_{𝑡}Y$$
Assertion	dvcnvrelem2	$$⊢\phi \to \left(F\left(C\right)\in \mathrm{int}\left(T\right)\left(Y\right)\wedge F^{-1}\in \left(N\mathrm{CnP}M\right)\left(F\left(C\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvcnvre.f	$$⊢\phi \to F:X\underset{cn}{⟶}ℝ$$
2		dvcnvre.d	$$⊢\phi \to \mathrm{dom}{F}_{ℝ}^{\prime }=X$$
3		dvcnvre.z	$$⊢\phi \to \neg 0\in \mathrm{ran}{F}_{ℝ}^{\prime }$$
4		dvcnvre.1	$$⊢\phi \to F:X\underset{1-1\; onto}{⟶}Y$$
5		dvcnvre.c	$$⊢\phi \to C\in X$$
6		dvcnvre.r	$$⊢\phi \to R\in {ℝ}^{+}$$
7		dvcnvre.s	$$⊢\phi \to \left[C-R,C+R\right]\subseteq X$$
8		dvcnvre.t	$$⊢T=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
9		dvcnvre.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
10		dvcnvre.m	$$⊢M=J{\upharpoonright }_{𝑡}X$$
11		dvcnvre.n	$$⊢N=J{\upharpoonright }_{𝑡}Y$$
12		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
13	8 12	eqeltri	$$⊢T\in \mathrm{Top}$$
14		f1ofo	$$⊢F:X\underset{1-1\; onto}{⟶}Y\to F:X\underset{onto}{⟶}Y$$
15		forn	$$⊢F:X\underset{onto}{⟶}Y\to \mathrm{ran}F=Y$$
16	4 14 15	3syl	$$⊢\phi \to \mathrm{ran}F=Y$$
17		cncff	$$⊢F:X\underset{cn}{⟶}ℝ\to F:X⟶ℝ$$
18		frn	$$⊢F:X⟶ℝ\to \mathrm{ran}F\subseteq ℝ$$
19	1 17 18	3syl	$$⊢\phi \to \mathrm{ran}F\subseteq ℝ$$
20	16 19	eqsstrrd	$$⊢\phi \to Y\subseteq ℝ$$
21		imassrn	$$⊢F\left[\left[C-R,C+R\right]\right]\subseteq \mathrm{ran}F$$
22	21 16	sseqtrid	$$⊢\phi \to F\left[\left[C-R,C+R\right]\right]\subseteq Y$$
23		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
24	8	unieqi	$$⊢\bigcup T=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
25	23 24	eqtr4i	$$⊢ℝ=\bigcup T$$
26	25	ntrss	$$⊢\left(T\in \mathrm{Top}\wedge Y\subseteq ℝ\wedge F\left[\left[C-R,C+R\right]\right]\subseteq Y\right)\to \mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\right)\subseteq \mathrm{int}\left(T\right)\left(Y\right)$$
27	13 20 22 26	mp3an2i	$$⊢\phi \to \mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\right)\subseteq \mathrm{int}\left(T\right)\left(Y\right)$$
28	1 2 3 4 5 6 7	dvcnvrelem1	$$⊢\phi \to F\left(C\right)\in \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(F\left[\left[C-R,C+R\right]\right]\right)$$
29	8	fveq2i	$$⊢\mathrm{int}\left(T\right)=\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
30	29	fveq1i	$$⊢\mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\right)=\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(F\left[\left[C-R,C+R\right]\right]\right)$$
31	28 30	eleqtrrdi	$$⊢\phi \to F\left(C\right)\in \mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\right)$$
32	27 31	sseldd	$$⊢\phi \to F\left(C\right)\in \mathrm{int}\left(T\right)\left(Y\right)$$
33		f1ocnv	$$⊢F:X\underset{1-1\; onto}{⟶}Y\to F^{-1}:Y\underset{1-1\; onto}{⟶}X$$
34		f1of	$$⊢F^{-1}:Y\underset{1-1\; onto}{⟶}X\to F^{-1}:Y⟶X$$
35	4 33 34	3syl	$$⊢\phi \to F^{-1}:Y⟶X$$
36		ffun	$$⊢F^{-1}:Y⟶X\to \mathrm{Fun}{F}^{-1}$$
37		funcnvres	$$⊢\mathrm{Fun}{F}^{-1}\to {\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}={F^{-1}\upharpoonright }_{F\left[\left[C-R,C+R\right]\right]}$$
38	35 36 37	3syl	$$⊢\phi \to {\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}={F^{-1}\upharpoonright }_{F\left[\left[C-R,C+R\right]\right]}$$
39		dvbsss	$$⊢\mathrm{dom}{F}_{ℝ}^{\prime }\subseteq ℝ$$
40	2 39	eqsstrrdi	$$⊢\phi \to X\subseteq ℝ$$
41		ax-resscn	$$⊢ℝ\subseteq ℂ$$
42	40 41	sstrdi	$$⊢\phi \to X\subseteq ℂ$$
43		cncfss	$$⊢\left(\left[C-R,C+R\right]\subseteq X\wedge X\subseteq ℂ\right)\to F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}\left[C-R,C+R\right]\subseteq F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}X$$
44	7 42 43	syl2anc	$$⊢\phi \to F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}\left[C-R,C+R\right]\subseteq F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}X$$
45		f1of1	$$⊢F:X\underset{1-1\; onto}{⟶}Y\to F:X\underset{1-1}{⟶}Y$$
46	4 45	syl	$$⊢\phi \to F:X\underset{1-1}{⟶}Y$$
47		f1ores	$$⊢\left(F:X\underset{1-1}{⟶}Y\wedge \left[C-R,C+R\right]\subseteq X\right)\to \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{1-1\; onto}{⟶}F\left[\left[C-R,C+R\right]\right]$$
48	46 7 47	syl2anc	$$⊢\phi \to \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{1-1\; onto}{⟶}F\left[\left[C-R,C+R\right]\right]$$
49	9	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=J{\upharpoonright }_{𝑡}ℝ$$
50	8 49	eqtri	$$⊢T=J{\upharpoonright }_{𝑡}ℝ$$
51	50	oveq1i	$$⊢T{\upharpoonright }_{𝑡}\left[C-R,C+R\right]=\left(J{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}\left[C-R,C+R\right]$$
52	9	cnfldtop	$$⊢J\in \mathrm{Top}$$
53	7 40	sstrd	$$⊢\phi \to \left[C-R,C+R\right]\subseteq ℝ$$
54		reex	$$⊢ℝ\in \mathrm{V}$$
55	54	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
56		restabs	$$⊢\left(J\in \mathrm{Top}\wedge \left[C-R,C+R\right]\subseteq ℝ\wedge ℝ\in \mathrm{V}\right)\to \left(J{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}\left[C-R,C+R\right]=J{\upharpoonright }_{𝑡}\left[C-R,C+R\right]$$
57	52 53 55 56	mp3an2i	$$⊢\phi \to \left(J{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}\left[C-R,C+R\right]=J{\upharpoonright }_{𝑡}\left[C-R,C+R\right]$$
58	51 57	syl5eq	$$⊢\phi \to T{\upharpoonright }_{𝑡}\left[C-R,C+R\right]=J{\upharpoonright }_{𝑡}\left[C-R,C+R\right]$$
59	40 5	sseldd	$$⊢\phi \to C\in ℝ$$
60	6	rpred	$$⊢\phi \to R\in ℝ$$
61	59 60	resubcld	$$⊢\phi \to C-R\in ℝ$$
62	59 60	readdcld	$$⊢\phi \to C+R\in ℝ$$
63		eqid	$$⊢T{\upharpoonright }_{𝑡}\left[C-R,C+R\right]=T{\upharpoonright }_{𝑡}\left[C-R,C+R\right]$$
64	8 63	icccmp	$$⊢\left(C-R\in ℝ\wedge C+R\in ℝ\right)\to T{\upharpoonright }_{𝑡}\left[C-R,C+R\right]\in \mathrm{Comp}$$
65	61 62 64	syl2anc	$$⊢\phi \to T{\upharpoonright }_{𝑡}\left[C-R,C+R\right]\in \mathrm{Comp}$$
66	58 65	eqeltrrd	$$⊢\phi \to J{\upharpoonright }_{𝑡}\left[C-R,C+R\right]\in \mathrm{Comp}$$
67		f1of	$$⊢\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{1-1\; onto}{⟶}F\left[\left[C-R,C+R\right]\right]\to \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]⟶F\left[\left[C-R,C+R\right]\right]$$
68	48 67	syl	$$⊢\phi \to \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]⟶F\left[\left[C-R,C+R\right]\right]$$
69	19 41	sstrdi	$$⊢\phi \to \mathrm{ran}F\subseteq ℂ$$
70	21 69	sstrid	$$⊢\phi \to F\left[\left[C-R,C+R\right]\right]\subseteq ℂ$$
71		rescncf	$$⊢\left[C-R,C+R\right]\subseteq X\to \left(F:X\underset{cn}{⟶}ℝ\to \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{cn}{⟶}ℝ\right)$$
72	7 1 71	sylc	$$⊢\phi \to \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{cn}{⟶}ℝ$$
73		cncffvrn	$$⊢\left(F\left[\left[C-R,C+R\right]\right]\subseteq ℂ\wedge \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{cn}{⟶}ℝ\right)\to \left(\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{cn}{⟶}F\left[\left[C-R,C+R\right]\right]\leftrightarrow \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]⟶F\left[\left[C-R,C+R\right]\right]\right)$$
74	70 72 73	syl2anc	$$⊢\phi \to \left(\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{cn}{⟶}F\left[\left[C-R,C+R\right]\right]\leftrightarrow \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]⟶F\left[\left[C-R,C+R\right]\right]\right)$$
75	68 74	mpbird	$$⊢\phi \to \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{cn}{⟶}F\left[\left[C-R,C+R\right]\right]$$
76		eqid	$$⊢J{\upharpoonright }_{𝑡}\left[C-R,C+R\right]=J{\upharpoonright }_{𝑡}\left[C-R,C+R\right]$$
77	9 76	cncfcnvcn	$$⊢\left(J{\upharpoonright }_{𝑡}\left[C-R,C+R\right]\in \mathrm{Comp}\wedge \left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{cn}{⟶}F\left[\left[C-R,C+R\right]\right]\right)\to \left(\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{1-1\; onto}{⟶}F\left[\left[C-R,C+R\right]\right]\leftrightarrow {\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}:F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}\left[C-R,C+R\right]\right)$$
78	66 75 77	syl2anc	$$⊢\phi \to \left(\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right):\left[C-R,C+R\right]\underset{1-1\; onto}{⟶}F\left[\left[C-R,C+R\right]\right]\leftrightarrow {\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}:F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}\left[C-R,C+R\right]\right)$$
79	48 78	mpbid	$$⊢\phi \to {\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}:F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}\left[C-R,C+R\right]$$
80	44 79	sseldd	$$⊢\phi \to {\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}:F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}X$$
81		eqid	$$⊢J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]=J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]$$
82	9 81 10	cncfcn	$$⊢\left(F\left[\left[C-R,C+R\right]\right]\subseteq ℂ\wedge X\subseteq ℂ\right)\to F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}X=\left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{Cn}M$$
83	70 42 82	syl2anc	$$⊢\phi \to F\left[\left[C-R,C+R\right]\right]\underset{cn}{⟶}X=\left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{Cn}M$$
84	80 83	eleqtrd	$$⊢\phi \to {\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}\in \left(\left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{Cn}M\right)$$
85	59 6	ltsubrpd	$$⊢\phi \to C-R<C$$
86	61 59 85	ltled	$$⊢\phi \to C-R\le C$$
87	59 6	ltaddrpd	$$⊢\phi \to C<C+R$$
88	59 62 87	ltled	$$⊢\phi \to C\le C+R$$
89		elicc2	$$⊢\left(C-R\in ℝ\wedge C+R\in ℝ\right)\to \left(C\in \left[C-R,C+R\right]\leftrightarrow \left(C\in ℝ\wedge C-R\le C\wedge C\le C+R\right)\right)$$
90	61 62 89	syl2anc	$$⊢\phi \to \left(C\in \left[C-R,C+R\right]\leftrightarrow \left(C\in ℝ\wedge C-R\le C\wedge C\le C+R\right)\right)$$
91	59 86 88 90	mpbir3and	$$⊢\phi \to C\in \left[C-R,C+R\right]$$
92		ffun	$$⊢F:X⟶ℝ\to \mathrm{Fun}F$$
93	1 17 92	3syl	$$⊢\phi \to \mathrm{Fun}F$$
94		fdm	$$⊢F:X⟶ℝ\to \mathrm{dom}F=X$$
95	1 17 94	3syl	$$⊢\phi \to \mathrm{dom}F=X$$
96	7 95	sseqtrrd	$$⊢\phi \to \left[C-R,C+R\right]\subseteq \mathrm{dom}F$$
97		funfvima2	$$⊢\left(\mathrm{Fun}F\wedge \left[C-R,C+R\right]\subseteq \mathrm{dom}F\right)\to \left(C\in \left[C-R,C+R\right]\to F\left(C\right)\in F\left[\left[C-R,C+R\right]\right]\right)$$
98	93 96 97	syl2anc	$$⊢\phi \to \left(C\in \left[C-R,C+R\right]\to F\left(C\right)\in F\left[\left[C-R,C+R\right]\right]\right)$$
99	91 98	mpd	$$⊢\phi \to F\left(C\right)\in F\left[\left[C-R,C+R\right]\right]$$
100	9	cnfldtopon	$$⊢J\in \mathrm{TopOn}\left(ℂ\right)$$
101		resttopon	$$⊢\left(J\in \mathrm{TopOn}\left(ℂ\right)\wedge F\left[\left[C-R,C+R\right]\right]\subseteq ℂ\right)\to J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\in \mathrm{TopOn}\left(F\left[\left[C-R,C+R\right]\right]\right)$$
102	100 70 101	sylancr	$$⊢\phi \to J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\in \mathrm{TopOn}\left(F\left[\left[C-R,C+R\right]\right]\right)$$
103		toponuni	$$⊢J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\in \mathrm{TopOn}\left(F\left[\left[C-R,C+R\right]\right]\right)\to F\left[\left[C-R,C+R\right]\right]=\bigcup \left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)$$
104	102 103	syl	$$⊢\phi \to F\left[\left[C-R,C+R\right]\right]=\bigcup \left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)$$
105	99 104	eleqtrd	$$⊢\phi \to F\left(C\right)\in \bigcup \left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)$$
106		eqid	$$⊢\bigcup \left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)=\bigcup \left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)$$
107	106	cncnpi	$$⊢\left({\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}\in \left(\left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{Cn}M\right)\wedge F\left(C\right)\in \bigcup \left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\right)\to {\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}\in \left(\left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M\right)\left(F\left(C\right)\right)$$
108	84 105 107	syl2anc	$$⊢\phi \to {\left({F\upharpoonright }_{\left[C-R,C+R\right]}\right)}^{-1}\in \left(\left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M\right)\left(F\left(C\right)\right)$$
109	38 108	eqeltrrd	$$⊢\phi \to {F^{-1}\upharpoonright }_{F\left[\left[C-R,C+R\right]\right]}\in \left(\left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M\right)\left(F\left(C\right)\right)$$
110	11	oveq1i	$$⊢N{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]=\left(J{\upharpoonright }_{𝑡}Y\right){\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]$$
111		ssexg	$$⊢\left(Y\subseteq ℝ\wedge ℝ\in \mathrm{V}\right)\to Y\in \mathrm{V}$$
112	20 54 111	sylancl	$$⊢\phi \to Y\in \mathrm{V}$$
113		restabs	$$⊢\left(J\in \mathrm{Top}\wedge F\left[\left[C-R,C+R\right]\right]\subseteq Y\wedge Y\in \mathrm{V}\right)\to \left(J{\upharpoonright }_{𝑡}Y\right){\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]=J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]$$
114	52 22 112 113	mp3an2i	$$⊢\phi \to \left(J{\upharpoonright }_{𝑡}Y\right){\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]=J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]$$
115	110 114	syl5eq	$$⊢\phi \to N{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]=J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]$$
116	115	oveq1d	$$⊢\phi \to \left(N{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M=\left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M$$
117	116	fveq1d	$$⊢\phi \to \left(\left(N{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M\right)\left(F\left(C\right)\right)=\left(\left(J{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M\right)\left(F\left(C\right)\right)$$
118	109 117	eleqtrrd	$$⊢\phi \to {F^{-1}\upharpoonright }_{F\left[\left[C-R,C+R\right]\right]}\in \left(\left(N{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M\right)\left(F\left(C\right)\right)$$
119	20 41	sstrdi	$$⊢\phi \to Y\subseteq ℂ$$
120		resttopon	$$⊢\left(J\in \mathrm{TopOn}\left(ℂ\right)\wedge Y\subseteq ℂ\right)\to J{\upharpoonright }_{𝑡}Y\in \mathrm{TopOn}\left(Y\right)$$
121	100 119 120	sylancr	$$⊢\phi \to J{\upharpoonright }_{𝑡}Y\in \mathrm{TopOn}\left(Y\right)$$
122	11 121	eqeltrid	$$⊢\phi \to N\in \mathrm{TopOn}\left(Y\right)$$
123		topontop	$$⊢N\in \mathrm{TopOn}\left(Y\right)\to N\in \mathrm{Top}$$
124	122 123	syl	$$⊢\phi \to N\in \mathrm{Top}$$
125		toponuni	$$⊢N\in \mathrm{TopOn}\left(Y\right)\to Y=\bigcup N$$
126	122 125	syl	$$⊢\phi \to Y=\bigcup N$$
127	22 126	sseqtrd	$$⊢\phi \to F\left[\left[C-R,C+R\right]\right]\subseteq \bigcup N$$
128	22 20	sstrd	$$⊢\phi \to F\left[\left[C-R,C+R\right]\right]\subseteq ℝ$$
129		difssd	$$⊢\phi \to ℝ\setminus Y\subseteq ℝ$$
130	128 129	unssd	$$⊢\phi \to F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\subseteq ℝ$$
131		ssun1	$$⊢F\left[\left[C-R,C+R\right]\right]\subseteq F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)$$
132	131	a1i	$$⊢\phi \to F\left[\left[C-R,C+R\right]\right]\subseteq F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)$$
133	25	ntrss	$$⊢\left(T\in \mathrm{Top}\wedge F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\subseteq ℝ\wedge F\left[\left[C-R,C+R\right]\right]\subseteq F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\right)\to \mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\right)\subseteq \mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\right)$$
134	13 130 132 133	mp3an2i	$$⊢\phi \to \mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\right)\subseteq \mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\right)$$
135	134 31	sseldd	$$⊢\phi \to F\left(C\right)\in \mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\right)$$
136		f1of	$$⊢F:X\underset{1-1\; onto}{⟶}Y\to F:X⟶Y$$
137	4 136	syl	$$⊢\phi \to F:X⟶Y$$
138	137 5	ffvelrnd	$$⊢\phi \to F\left(C\right)\in Y$$
139	135 138	elind	$$⊢\phi \to F\left(C\right)\in \left(\mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\right)\cap Y\right)$$
140		eqid	$$⊢T{\upharpoonright }_{𝑡}Y=T{\upharpoonright }_{𝑡}Y$$
141	25 140	restntr	$$⊢\left(T\in \mathrm{Top}\wedge Y\subseteq ℝ\wedge F\left[\left[C-R,C+R\right]\right]\subseteq Y\right)\to \mathrm{int}\left(T{\upharpoonright }_{𝑡}Y\right)\left(F\left[\left[C-R,C+R\right]\right]\right)=\mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\right)\cap Y$$
142	13 20 22 141	mp3an2i	$$⊢\phi \to \mathrm{int}\left(T{\upharpoonright }_{𝑡}Y\right)\left(F\left[\left[C-R,C+R\right]\right]\right)=\mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\right)\cap Y$$
143		restabs	$$⊢\left(J\in \mathrm{Top}\wedge Y\subseteq ℝ\wedge ℝ\in \mathrm{V}\right)\to \left(J{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}Y=J{\upharpoonright }_{𝑡}Y$$
144	52 20 55 143	mp3an2i	$$⊢\phi \to \left(J{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}Y=J{\upharpoonright }_{𝑡}Y$$
145	50	oveq1i	$$⊢T{\upharpoonright }_{𝑡}Y=\left(J{\upharpoonright }_{𝑡}ℝ\right){\upharpoonright }_{𝑡}Y$$
146	144 145 11	3eqtr4g	$$⊢\phi \to T{\upharpoonright }_{𝑡}Y=N$$
147	146	fveq2d	$$⊢\phi \to \mathrm{int}\left(T{\upharpoonright }_{𝑡}Y\right)=\mathrm{int}\left(N\right)$$
148	147	fveq1d	$$⊢\phi \to \mathrm{int}\left(T{\upharpoonright }_{𝑡}Y\right)\left(F\left[\left[C-R,C+R\right]\right]\right)=\mathrm{int}\left(N\right)\left(F\left[\left[C-R,C+R\right]\right]\right)$$
149	142 148	eqtr3d	$$⊢\phi \to \mathrm{int}\left(T\right)\left(F\left[\left[C-R,C+R\right]\right]\cup \left(ℝ\setminus Y\right)\right)\cap Y=\mathrm{int}\left(N\right)\left(F\left[\left[C-R,C+R\right]\right]\right)$$
150	139 149	eleqtrd	$$⊢\phi \to F\left(C\right)\in \mathrm{int}\left(N\right)\left(F\left[\left[C-R,C+R\right]\right]\right)$$
151	126	feq2d	$$⊢\phi \to \left(F^{-1}:Y⟶X\leftrightarrow F^{-1}:\bigcup N⟶X\right)$$
152	35 151	mpbid	$$⊢\phi \to F^{-1}:\bigcup N⟶X$$
153		resttopon	$$⊢\left(J\in \mathrm{TopOn}\left(ℂ\right)\wedge X\subseteq ℂ\right)\to J{\upharpoonright }_{𝑡}X\in \mathrm{TopOn}\left(X\right)$$
154	100 42 153	sylancr	$$⊢\phi \to J{\upharpoonright }_{𝑡}X\in \mathrm{TopOn}\left(X\right)$$
155	10 154	eqeltrid	$$⊢\phi \to M\in \mathrm{TopOn}\left(X\right)$$
156		toponuni	$$⊢M\in \mathrm{TopOn}\left(X\right)\to X=\bigcup M$$
157		feq3	$$⊢X=\bigcup M\to \left(F^{-1}:\bigcup N⟶X\leftrightarrow F^{-1}:\bigcup N⟶\bigcup M\right)$$
158	155 156 157	3syl	$$⊢\phi \to \left(F^{-1}:\bigcup N⟶X\leftrightarrow F^{-1}:\bigcup N⟶\bigcup M\right)$$
159	152 158	mpbid	$$⊢\phi \to F^{-1}:\bigcup N⟶\bigcup M$$
160		eqid	$$⊢\bigcup N=\bigcup N$$
161		eqid	$$⊢\bigcup M=\bigcup M$$
162	160 161	cnprest	$$⊢\left(\left(N\in \mathrm{Top}\wedge F\left[\left[C-R,C+R\right]\right]\subseteq \bigcup N\right)\wedge \left(F\left(C\right)\in \mathrm{int}\left(N\right)\left(F\left[\left[C-R,C+R\right]\right]\right)\wedge F^{-1}:\bigcup N⟶\bigcup M\right)\right)\to \left(F^{-1}\in \left(N\mathrm{CnP}M\right)\left(F\left(C\right)\right)\leftrightarrow {F^{-1}\upharpoonright }_{F\left[\left[C-R,C+R\right]\right]}\in \left(\left(N{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M\right)\left(F\left(C\right)\right)\right)$$
163	124 127 150 159 162	syl22anc	$$⊢\phi \to \left(F^{-1}\in \left(N\mathrm{CnP}M\right)\left(F\left(C\right)\right)\leftrightarrow {F^{-1}\upharpoonright }_{F\left[\left[C-R,C+R\right]\right]}\in \left(\left(N{\upharpoonright }_{𝑡}F\left[\left[C-R,C+R\right]\right]\right)\mathrm{CnP}M\right)\left(F\left(C\right)\right)\right)$$
164	118 163	mpbird	$$⊢\phi \to F^{-1}\in \left(N\mathrm{CnP}M\right)\left(F\left(C\right)\right)$$
165	32 164	jca	$$⊢\phi \to \left(F\left(C\right)\in \mathrm{int}\left(T\right)\left(Y\right)\wedge F^{-1}\in \left(N\mathrm{CnP}M\right)\left(F\left(C\right)\right)\right)$$