Theorem hmeontr

Description: Homeomorphisms preserve interiors. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	hmeoopn.1	$$⊢X=\bigcup J$$
Assertion	hmeontr	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \mathrm{int}\left(K\right)\left(F\left[A\right]\right)=F\left[\mathrm{int}\left(J\right)\left(A\right)\right]$$

Proof

Step	Hyp	Ref	Expression
1		hmeoopn.1	$$⊢X=\bigcup J$$
2		hmeocn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F\in \left(J\mathrm{Cn}K\right)$$
3	2	adantr	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F\in \left(J\mathrm{Cn}K\right)$$
4		imassrn	$$⊢F\left[A\right]\subseteq \mathrm{ran}F$$
5		eqid	$$⊢\bigcup K=\bigcup K$$
6	1 5	hmeof1o	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F:X\underset{1-1\; onto}{⟶}\bigcup K$$
7	6	adantr	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F:X\underset{1-1\; onto}{⟶}\bigcup K$$
8		f1ofo	$$⊢F:X\underset{1-1\; onto}{⟶}\bigcup K\to F:X\underset{onto}{⟶}\bigcup K$$
9		forn	$$⊢F:X\underset{onto}{⟶}\bigcup K\to \mathrm{ran}F=\bigcup K$$
10	7 8 9	3syl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \mathrm{ran}F=\bigcup K$$
11	4 10	sseqtrid	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F\left[A\right]\subseteq \bigcup K$$
12	5	cnntri	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge F\left[A\right]\subseteq \bigcup K\right)\to F^{-1}\left[\mathrm{int}\left(K\right)\left(F\left[A\right]\right)\right]\subseteq \mathrm{int}\left(J\right)\left(F^{-1}\left[F\left[A\right]\right]\right)$$
13	3 11 12	syl2anc	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F^{-1}\left[\mathrm{int}\left(K\right)\left(F\left[A\right]\right)\right]\subseteq \mathrm{int}\left(J\right)\left(F^{-1}\left[F\left[A\right]\right]\right)$$
14		f1of1	$$⊢F:X\underset{1-1\; onto}{⟶}\bigcup K\to F:X\underset{1-1}{⟶}\bigcup K$$
15	7 14	syl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F:X\underset{1-1}{⟶}\bigcup K$$
16		f1imacnv	$$⊢\left(F:X\underset{1-1}{⟶}\bigcup K\wedge A\subseteq X\right)\to F^{-1}\left[F\left[A\right]\right]=A$$
17	15 16	sylancom	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F^{-1}\left[F\left[A\right]\right]=A$$
18	17	fveq2d	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \mathrm{int}\left(J\right)\left(F^{-1}\left[F\left[A\right]\right]\right)=\mathrm{int}\left(J\right)\left(A\right)$$
19	13 18	sseqtrd	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F^{-1}\left[\mathrm{int}\left(K\right)\left(F\left[A\right]\right)\right]\subseteq \mathrm{int}\left(J\right)\left(A\right)$$
20		f1ofun	$$⊢F:X\underset{1-1\; onto}{⟶}\bigcup K\to \mathrm{Fun}F$$
21	7 20	syl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \mathrm{Fun}F$$
22		cntop2	$$⊢F\in \left(J\mathrm{Cn}K\right)\to K\in \mathrm{Top}$$
23	3 22	syl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to K\in \mathrm{Top}$$
24	5	ntrss3	$$⊢\left(K\in \mathrm{Top}\wedge F\left[A\right]\subseteq \bigcup K\right)\to \mathrm{int}\left(K\right)\left(F\left[A\right]\right)\subseteq \bigcup K$$
25	23 11 24	syl2anc	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \mathrm{int}\left(K\right)\left(F\left[A\right]\right)\subseteq \bigcup K$$
26	25 10	sseqtrrd	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \mathrm{int}\left(K\right)\left(F\left[A\right]\right)\subseteq \mathrm{ran}F$$
27		funimass1	$$⊢\left(\mathrm{Fun}F\wedge \mathrm{int}\left(K\right)\left(F\left[A\right]\right)\subseteq \mathrm{ran}F\right)\to \left(F^{-1}\left[\mathrm{int}\left(K\right)\left(F\left[A\right]\right)\right]\subseteq \mathrm{int}\left(J\right)\left(A\right)\to \mathrm{int}\left(K\right)\left(F\left[A\right]\right)\subseteq F\left[\mathrm{int}\left(J\right)\left(A\right)\right]\right)$$
28	21 26 27	syl2anc	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \left(F^{-1}\left[\mathrm{int}\left(K\right)\left(F\left[A\right]\right)\right]\subseteq \mathrm{int}\left(J\right)\left(A\right)\to \mathrm{int}\left(K\right)\left(F\left[A\right]\right)\subseteq F\left[\mathrm{int}\left(J\right)\left(A\right)\right]\right)$$
29	19 28	mpd	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \mathrm{int}\left(K\right)\left(F\left[A\right]\right)\subseteq F\left[\mathrm{int}\left(J\right)\left(A\right)\right]$$
30		hmeocnvcn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F^{-1}\in \left(K\mathrm{Cn}J\right)$$
31	1	cnntri	$$⊢\left(F^{-1}\in \left(K\mathrm{Cn}J\right)\wedge A\subseteq X\right)\to {F^{-1}}^{-1}\left[\mathrm{int}\left(J\right)\left(A\right)\right]\subseteq \mathrm{int}\left(K\right)\left({F^{-1}}^{-1}\left[A\right]\right)$$
32	30 31	sylan	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to {F^{-1}}^{-1}\left[\mathrm{int}\left(J\right)\left(A\right)\right]\subseteq \mathrm{int}\left(K\right)\left({F^{-1}}^{-1}\left[A\right]\right)$$
33		imacnvcnv	$$⊢{F^{-1}}^{-1}\left[\mathrm{int}\left(J\right)\left(A\right)\right]=F\left[\mathrm{int}\left(J\right)\left(A\right)\right]$$
34		imacnvcnv	$$⊢{F^{-1}}^{-1}\left[A\right]=F\left[A\right]$$
35	34	fveq2i	$$⊢\mathrm{int}\left(K\right)\left({F^{-1}}^{-1}\left[A\right]\right)=\mathrm{int}\left(K\right)\left(F\left[A\right]\right)$$
36	32 33 35	3sstr3g	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to F\left[\mathrm{int}\left(J\right)\left(A\right)\right]\subseteq \mathrm{int}\left(K\right)\left(F\left[A\right]\right)$$
37	29 36	eqssd	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge A\subseteq X\right)\to \mathrm{int}\left(K\right)\left(F\left[A\right]\right)=F\left[\mathrm{int}\left(J\right)\left(A\right)\right]$$