Theorem hmeofn

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

	Ref	Expression
Assertion	hmeofn	|- Homeo Fn ( Top X. Top )

Proof

Step	Hyp	Ref	Expression
1		df-hmeo	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
2		ovex	|- ( j Cn k ) e. _V
3	2	rabex	|- { f e. ( j Cn k ) | `' f e. ( k Cn j ) } e. _V
4	1 3	fnmpoi	|- Homeo Fn ( Top X. Top )