Theorem hmeoimaf1o

Description: The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Hypothesis	hmeoimaf1o.1	$$⊢G=\left(x\in J⟼F\left[x\right]\right)$$
Assertion	hmeoimaf1o	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to G:J\underset{1-1\; onto}{⟶}K$$

Proof

Step	Hyp	Ref	Expression
1		hmeoimaf1o.1	$$⊢G=\left(x\in J⟼F\left[x\right]\right)$$
2		hmeoima	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge x\in J\right)\to F\left[x\right]\in K$$
3		hmeocn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F\in \left(J\mathrm{Cn}K\right)$$
4		cnima	$$⊢\left(F\in \left(J\mathrm{Cn}K\right)\wedge y\in K\right)\to F^{-1}\left[y\right]\in J$$
5	3 4	sylan	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge y\in K\right)\to F^{-1}\left[y\right]\in J$$
6		eqid	$$⊢\bigcup J=\bigcup J$$
7		eqid	$$⊢\bigcup K=\bigcup K$$
8	6 7	hmeof1o	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F:\bigcup J\underset{1-1\; onto}{⟶}\bigcup K$$
9	8	adantr	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to F:\bigcup J\underset{1-1\; onto}{⟶}\bigcup K$$
10		f1of1	$$⊢F:\bigcup J\underset{1-1\; onto}{⟶}\bigcup K\to F:\bigcup J\underset{1-1}{⟶}\bigcup K$$
11	9 10	syl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to F:\bigcup J\underset{1-1}{⟶}\bigcup K$$
12		elssuni	$$⊢x\in J\to x\subseteq \bigcup J$$
13	12	ad2antrl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to x\subseteq \bigcup J$$
14		cnvimass	$$⊢F^{-1}\left[y\right]\subseteq \mathrm{dom}F$$
15		f1dm	$$⊢F:\bigcup J\underset{1-1}{⟶}\bigcup K\to \mathrm{dom}F=\bigcup J$$
16	11 15	syl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to \mathrm{dom}F=\bigcup J$$
17	14 16	sseqtrid	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to F^{-1}\left[y\right]\subseteq \bigcup J$$
18		f1imaeq	$$⊢\left(F:\bigcup J\underset{1-1}{⟶}\bigcup K\wedge \left(x\subseteq \bigcup J\wedge F^{-1}\left[y\right]\subseteq \bigcup J\right)\right)\to \left(F\left[x\right]=F\left[F^{-1}\left[y\right]\right]\leftrightarrow x=F^{-1}\left[y\right]\right)$$
19	11 13 17 18	syl12anc	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to \left(F\left[x\right]=F\left[F^{-1}\left[y\right]\right]\leftrightarrow x=F^{-1}\left[y\right]\right)$$
20		f1ofo	$$⊢F:\bigcup J\underset{1-1\; onto}{⟶}\bigcup K\to F:\bigcup J\underset{onto}{⟶}\bigcup K$$
21	9 20	syl	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to F:\bigcup J\underset{onto}{⟶}\bigcup K$$
22		elssuni	$$⊢y\in K\to y\subseteq \bigcup K$$
23	22	ad2antll	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to y\subseteq \bigcup K$$
24		foimacnv	$$⊢\left(F:\bigcup J\underset{onto}{⟶}\bigcup K\wedge y\subseteq \bigcup K\right)\to F\left[F^{-1}\left[y\right]\right]=y$$
25	21 23 24	syl2anc	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to F\left[F^{-1}\left[y\right]\right]=y$$
26	25	eqeq2d	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to \left(F\left[x\right]=F\left[F^{-1}\left[y\right]\right]\leftrightarrow F\left[x\right]=y\right)$$
27		eqcom	$$⊢F\left[x\right]=y\leftrightarrow y=F\left[x\right]$$
28	26 27	bitrdi	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to \left(F\left[x\right]=F\left[F^{-1}\left[y\right]\right]\leftrightarrow y=F\left[x\right]\right)$$
29	19 28	bitr3d	$$⊢\left(F\in \left(J\mathrm{Homeo}K\right)\wedge \left(x\in J\wedge y\in K\right)\right)\to \left(x=F^{-1}\left[y\right]\leftrightarrow y=F\left[x\right]\right)$$
30	1 2 5 29	f1o2d	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to G:J\underset{1-1\; onto}{⟶}K$$