Theorem hmeocnv

Description: The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Assertion	hmeocnv	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F^{-1}\in \left(K\mathrm{Homeo}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		hmeocnvcn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F^{-1}\in \left(K\mathrm{Cn}J\right)$$
2		hmeocn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F\in \left(J\mathrm{Cn}K\right)$$
3		eqid	$$⊢\bigcup J=\bigcup J$$
4		eqid	$$⊢\bigcup K=\bigcup K$$
5	3 4	cnf	$$⊢F\in \left(J\mathrm{Cn}K\right)\to F:\bigcup J⟶\bigcup K$$
6		frel	$$⊢F:\bigcup J⟶\bigcup K\to \mathrm{Rel}F$$
7	2 5 6	3syl	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to \mathrm{Rel}F$$
8		dfrel2	$$⊢\mathrm{Rel}F\leftrightarrow {F^{-1}}^{-1}=F$$
9	7 8	sylib	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to {F^{-1}}^{-1}=F$$
10	9 2	eqeltrd	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to {F^{-1}}^{-1}\in \left(J\mathrm{Cn}K\right)$$
11		ishmeo	$$⊢F^{-1}\in \left(K\mathrm{Homeo}J\right)\leftrightarrow \left(F^{-1}\in \left(K\mathrm{Cn}J\right)\wedge {F^{-1}}^{-1}\in \left(J\mathrm{Cn}K\right)\right)$$
12	1 10 11	sylanbrc	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F^{-1}\in \left(K\mathrm{Homeo}J\right)$$