Theorem hmeofn

Description: The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Assertion	hmeofn	$$⊢\mathrm{Homeo}Fn\left(\mathrm{Top}\times \mathrm{Top}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-hmeo	$$⊢\mathrm{Homeo}=\left(j\in \mathrm{Top},k\in \mathrm{Top}⟼\left\{f\in \left(j\mathrm{Cn}k\right)|f^{-1}\in \left(k\mathrm{Cn}j\right)\right\}\right)$$
2		ovex	$$⊢j\mathrm{Cn}k\in \mathrm{V}$$
3	2	rabex	$$⊢\left\{f\in \left(j\mathrm{Cn}k\right)|f^{-1}\in \left(k\mathrm{Cn}j\right)\right\}\in \mathrm{V}$$
4	1 3	fnmpoi	$$⊢\mathrm{Homeo}Fn\left(\mathrm{Top}\times \mathrm{Top}\right)$$