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 × Top )

Proof

Step	Hyp	Ref	Expression
1		df-hmeo	⊢ Homeo = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( 𝑗 Cn 𝑘 ) ∣ ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 ) } )
2		ovex	⊢ ( 𝑗 Cn 𝑘 ) ∈ V
3	2	rabex	⊢ { 𝑓 ∈ ( 𝑗 Cn 𝑘 ) ∣ ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 ) } ∈ V
4	1 3	fnmpoi	⊢ Homeo Fn ( Top × Top )